@@ -1,14 +1,14 @@
1−module System.Concurrency.Sessions
1+module System.Concurrency.Channels
3import System.Concurrency.Raw
3import System.Concurrency.Raw
5−||| A Session is a connection between two processes. Sessions can be created
5+||| A Channel is a connection between two processes. Channels can be created
6||| either using 'listen' to wait for an incoming connection, or 'connect'
6||| either using 'listen' to wait for an incoming connection, or 'connect'
7||| which initiates a connection to another process.
7||| which initiates a connection to another process.
8−||| Sessions cannot be passed between processes.
8+||| Channels cannot (yet) be passed between processes.
10−data Session : Type where
10+data Channel : Type where
11− MkConc : (pid : Ptr) -> (ch_id : Int) -> Session
11+ MkConc : (pid : Ptr) -> (ch_id : Int) -> Channel
13||| A PID is a process identifier, as returned by `spawn`
13||| A PID is a process identifier, as returned by `spawn`
@@ -17,13 +17,13 @@ data PID : Type where
18||| Spawn a process in a new thread, returning the process ID
18||| Spawn a process in a new thread, returning the process ID
20−spawn : IO () -> IO PID
20+spawn : (process : IO ()) -> IO PID
21spawn proc = do pid <- fork proc
21spawn proc = do pid <- fork proc
22 pure (MkPID pid)
22 pure (MkPID pid)
24||| Create a channel which connects this process to another process
24||| Create a channel which connects this process to another process
26−connect : (proc : PID) -> IO (Maybe Session)
26+connect : (pid : PID) -> IO (Maybe Channel)
27connect (MkPID pid) = do ch_id <- sendToThread pid 0 ()
27connect (MkPID pid) = do ch_id <- sendToThread pid 0 ()
28 if (ch_id /= 0)
28 if (ch_id /= 0)
29 then pure (Just (MkConc pid ch_id))
29 then pure (Just (MkConc pid ch_id))
@@ -32,7 +32,7 @@ connect (MkPID pid) = do ch_id <- sendToThread pid 0 ()
32||| Listen for incoming connections. If another process has initiated a
32||| Listen for incoming connections. If another process has initiated a
33||| communication with this process, returns a channel
33||| communication with this process, returns a channel
35−listen : (timeout : Int) -> IO (Maybe Session)
35+listen : (timeout : Int) -> IO (Maybe Channel)
36listen timeout = do checkMsgsTimeout timeout
36listen timeout = do checkMsgsTimeout timeout
37 Just (client, ch_id) <- listenMsgs
37 Just (client, ch_id) <- listenMsgs
38 | Nothing => pure Nothing
38 | Nothing => pure Nothing
@@ -46,7 +46,7 @@ listen timeout = do checkMsgsTimeout timeout
46||| a protocol (externally checked) which ensures that the message send
46||| a protocol (externally checked) which ensures that the message send
47||| is of type expected by the receiver.
47||| is of type expected by the receiver.
49−unsafeSend : Session -> (val : a) -> IO Bool
49+unsafeSend : Channel -> (val : a) -> IO Bool
50unsafeSend (MkConc pid ch_id) val
50unsafeSend (MkConc pid ch_id) val
51 = do ok <- sendToThread pid ch_id val
51 = do ok <- sendToThread pid ch_id val
52 pure (ok /= 0)
52 pure (ok /= 0)
@@ -58,6 +58,6 @@ unsafeSend (MkConc pid ch_id) val
58||| a protocol (externally checked) which ensures that the message received
58||| a protocol (externally checked) which ensures that the message received
59||| is of the type given by the sender.
59||| is of the type given by the sender.
61−unsafeRecv : (a : Type) -> Session -> IO (Maybe a)
61+unsafeRecv : (a : Type) -> Channel -> IO (Maybe a)
62unsafeRecv a (MkConc pid ch_id) = getMsgFrom {a} pid ch_id
62unsafeRecv a (MkConc pid ch_id) = getMsgFrom {a} pid ch_id