module Make:Binary_session.Binary_processwith type 'a io = 'a Lwt.t and type chan_endpoint = (Lwt_io.input_channel * Lwt_io.output_channel)
Binary_session.Binary_process.type 'a io
'a.type chan_endpoint
type ([> ], [> ]) session
'a is the sequence of operations from the point of view from the first process and 'b
its dual is the sequence of operations from the point of view of the second process.type ('a, 'b, 'c) process
'a. The type 'b represents the next allowed
sequnce of operations and 'c represents the sequence of operations after performing the first operation
in 'b.val send : 'a ->
(unit,
([ `Send of 'a * ([> ] as 'b) ], [ `Recv of 'a * ([> ] as 'c) ])
session,
('b, 'c) session)
processsend v creates a process which is capable of sending a value of type 'a (v) to the other process.val recv : unit ->
('a,
([ `Recv of 'a * ([> ] as 'b) ], [ `Send of 'a * ([> ] as 'c) ])
session,
('b, 'c) session)
processrecv () creates a process which is capable of receiving a value of type 'a to the other process.val offer : ('e, ([> ] as 'a, [> ] as 'b) session, 'f)
process ->
('e, ([> ] as 'c, [> ] as 'd) session, 'f)
process ->
('e,
([ `Offer of
('a, 'b) session *
('c, 'd) session ],
[ `Choice of
('b, 'a) session *
('d, 'c) session ])
session, 'f)
processoffer left_choice right_choice creates a process which allows the other process to make a choice between
two choices left_choice and right_choice.val choose_left : ('e, ([> ] as 'a, [> ] as 'b) session, 'f)
process ->
('e,
([ `Choice of
('a, 'b) session *
([> ] as 'c, [> ] as 'd) session ],
[ `Offer of
('b, 'a) session *
('d, 'c) session ])
session, 'f)
processchoose_left left_choice creates a process which internally chooses left_choice and communicates this choice
to the other process.val choose_right : ('e, ([> ] as 'a, [> ] as 'b) session, 'f)
process ->
('e,
([ `Choice of
([> ] as 'c, [> ] as 'd) session *
('a, 'b) session ],
[ `Offer of
('d, 'c) session *
('b, 'a) session ])
session, 'f)
processchoose_right right_choice creates a process which internally chooses rigth_choice and communicates this choice
to the other process.val stop : 'a ->
('a, ([ `Stop ], [ `Stop ]) session, unit)
processstop v creates a process which stops (is not capable of performing any further operations) and returns a
value v.val lift_io : 'a io ->
('a, 'b, 'b) processlift_io io lifts the io computation into the process. The processes' capabilities are not altered.val return : 'a -> ('a, 'b, 'b) processreturn v creates a process which returns v its capabilities are not altered.val (>>=) : ('a, 'b, 'c) process ->
('a -> ('d, 'c, 'e) process) ->
('d, 'b, 'e) processp1 >>= f creates a process which is the composition of running p1 then applying.val run_processes : ('a, ([> ] as 'b, [> ] as 'c) session, unit)
process ->
('d, ('c, 'b) session, unit)
process ->
((unit -> 'a io) *
(unit -> 'd io))
iorun_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). The result is a
Binary_session.IO.t returning a pair of functions which may be invoked to run each process.
Note, the channel that is opened between the two processes is closed when the processes have completed.