| (>>=) [Binary_session.IO] | bind t f is a thread which first waits for the thread t to terminate and then, behaves as the application of
function f to the return value of t.
|
| (>>=) [Binary_session.Binary_process] | p1 >>= f creates a process which is the composition of running p1 then applying.
|
C | |
| choose_left [Binary_session.Binary_process] | choose_left left_choice creates a process which internally chooses left_choice and communicates this choice
to the other process.
|
| choose_right [Binary_session.Binary_process] | choose_right right_choice creates a process which internally chooses rigth_choice and communicates this choice
to the other process.
|
| close_channel [Binary_session.IO] | close_channel c will close the given channel c.
|
L | |
| lift_io [Binary_session.Binary_process] | lift_io io lifts the io computation into the process.
|
M | |
| make_channel [Binary_session.IO] | make_channel () will return a new communication channel Binary_session.IO.chan.
|
O | |
| offer [Binary_session.Binary_process] | offer left_choice right_choice creates a process which allows the other process to make a choice between
two choices left_choice and right_choice.
|
R | |
| read_channel [Binary_session.IO] | read_channel end_point reads a marshalled value from end_point and returns it.
|
| recv [Binary_session.Binary_process] | recv () creates a process which is capable of receiving a value of type 'a to the other process.
|
| return [Binary_session.IO] | return v creates a light weight thread returning v.
|
| return [Binary_session.Binary_process] | return v creates a process which returns v its capabilities are not altered.
|
| run_processes [Binary_session.Binary_process] | run_process p1 p2 will run two processes p1 and p2 which have dual session types and which have
unit as their end state capabilities (i.e., are complete processes).
|
S | |
| send [Binary_session.Binary_process] | send v creates a process which is capable of sending a value of type 'a (v) to the other process.
|
| stop [Binary_session.Binary_process] | stop v creates a process which stops (is not capable of performing any further operations) and returns a
value v.
|
W | |
| write_channel [Binary_session.IO] | write_channel v flags end_point marshals the value v according to flags and writes it to end_point.
|