Up  

Functor Binary_session.Make

module Make (I : IO) : Binary_process  with type 'a io = 'a I.t and type chan_endpoint = I.chan_endpoint
Functor to create a module of type Binary_session.Binary_process given a message module I of type Binary_session.IO.
Parameters:
I : IO 
type 'a io
The abstract monadic type representing a computation returning 'a.
type chan_endpoint
The abstract type representing one end of a communication channel.
type ([>  ], [>  ]) session
The type representing a communication protocol made up of a sequence of operations between two processes. The type '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
The type representing a process returning a value of type '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)
       process
send 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)
       process
recv () 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)
       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.
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)
       process
choose_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)
       process
choose_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)
       process
stop 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) process
lift_io io lifts the io computation into the process. The processes' capabilities are not altered.
val return : 'a -> ('a, 'b, 'b) process
return 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) process
p1 >>= 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))
       io
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). 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.