git.iko.soy/Idris-dev
on 308efea help sign in
Idris-dev/lib/System/Concurrency/Process.idr
69 lines 1.8 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 fmap f (lift a) = lift (fmap 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 return = lift . return
27 (lift io) >>= k = lift (do x <- io
28 case k x of
29 lift v => v)
31run : Process msg x -> IO x
32run (lift prog) = prog
34-- Get current process ID
36myID : Process msg (ProcID msg)
37myID = lift (return (MkPID prim__vm))
39-- Send a message to another process
41send : ProcID msg -> msg -> Process msg ()
42send (MkPID p) m = lift (sendToThread p (prim__vm, m))
44-- Return whether a message is waiting in the queue
46msgWaiting : Process msg Bool
47msgWaiting = lift checkMsgs
49-- Receive a message - blocks if there is no message waiting
51recv : Process msg msg
52recv {msg} = do (senderid, m) <- lift get
53 return m
54 where get : IO (Ptr, msg)
55 get = getMsg
57-- receive a message, and return with the sender's process ID.
59recvWithSender : Process msg (ProcID msg, msg)
60recvWithSender {msg}
61 = do (senderid, m) <- lift get
62 return (MkPID senderid, m)
63 where get : IO (Ptr, msg)
64 get = getMsg
66create : |(thread : Process msg ()) -> Process msg (ProcID msg)
67create (lift p) = do ptr <- lift (fork p)
68 return (MkPID ptr)