git.iko.soy/Idris-dev
on 40ce0ca help sign in
Idris-dev/lib/System/Concurrency/Process.idr
62 lines 1.6 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 : Set) -> Set -> Set where
16 lift : IO a -> Process msg a
18instance Monad (Process msg) where
19 return = lift . return
20 (lift io) >>= k = lift (do x <- io
21 case k x of
22 lift v => v)
24run : Process msg x -> IO x
25run (lift prog) = prog
27-- Get current process ID
29myID : Process msg (ProcID msg)
30myID = lift (return (MkPID prim__vm))
32-- Send a message to another process
34send : ProcID msg -> msg -> Process msg ()
35send (MkPID p) m = lift (sendToThread p (prim__vm, m))
37-- Return whether a message is waiting in the queue
39msgWaiting : Process msg Bool
40msgWaiting = lift checkMsgs
42-- Receive a message - blocks if there is no message waiting
44recv : Process msg msg
45recv {msg} = do (senderid, m) <- lift get
46 return m
47 where get : IO (Ptr, msg)
48 get = getMsg
50-- 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 : |(thread : Process msg ()) -> Process msg (ProcID msg)
60create (lift p) = do ptr <- lift (fork p)
61 return (MkPID ptr)