@@ -1,14 +1,14 @@
1−module System.Concurrency.Sessions
1+module System.Concurrency.Channels
22
33import System.Concurrency.Raw
44
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
66||| either using 'listen' to wait for an incoming connection, or 'connect'
77||| which initiates a connection to another process.
8−||| Sessions cannot be passed between processes.
8+||| Channels cannot (yet) be passed between processes.
99export
10−data Session : Type where
11− MkConc : (pid : Ptr) -> (ch_id : Int) -> Session
10+data Channel : Type where
11+ MkConc : (pid : Ptr) -> (ch_id : Int) -> Channel
1212
1313||| A PID is a process identifier, as returned by `spawn`
1414export
@@ -17,13 +17,13 @@ data PID : Type where
1717
1818||| Spawn a process in a new thread, returning the process ID
1919export
20−spawn : IO () -> IO PID
20+spawn : (process : IO ()) -> IO PID
2121spawn proc = do pid <- fork proc
2222 pure (MkPID pid)
2323
2424||| Create a channel which connects this process to another process
2525export
26−connect : (proc : PID) -> IO (Maybe Session)
26+connect : (pid : PID) -> IO (Maybe Channel)
2727connect (MkPID pid) = do ch_id <- sendToThread pid 0 ()
2828 if (ch_id /= 0)
2929 then pure (Just (MkConc pid ch_id))
@@ -32,7 +32,7 @@ connect (MkPID pid) = do ch_id <- sendToThread pid 0 ()
3232||| Listen for incoming connections. If another process has initiated a
3333||| communication with this process, returns a channel
3434export
35−listen : (timeout : Int) -> IO (Maybe Session)
35+listen : (timeout : Int) -> IO (Maybe Channel)
3636listen timeout = do checkMsgsTimeout timeout
3737 Just (client, ch_id) <- listenMsgs
3838 | Nothing => pure Nothing
@@ -46,7 +46,7 @@ listen timeout = do checkMsgsTimeout timeout
4646||| a protocol (externally checked) which ensures that the message send
4747||| is of type expected by the receiver.
4848export
49−unsafeSend : Session -> (val : a) -> IO Bool
49+unsafeSend : Channel -> (val : a) -> IO Bool
5050unsafeSend (MkConc pid ch_id) val
5151 = do ok <- sendToThread pid ch_id val
5252 pure (ok /= 0)
@@ -58,6 +58,6 @@ unsafeSend (MkConc pid ch_id) val
5858||| a protocol (externally checked) which ensures that the message received
5959||| is of the type given by the sender.
6060export
61−unsafeRecv : (a : Type) -> Session -> IO (Maybe a)
61+unsafeRecv : (a : Type) -> Channel -> IO (Maybe a)
6262unsafeRecv a (MkConc pid ch_id) = getMsgFrom {a} pid ch_id
6363