Demo Polarized Protocol

datasort stype = 
| psend of (vt@ype)
| precv of (vt@ype)
| pclose
| pwait
| pseq of (stype, stype)

stadef :: = pseq
absvtype channel (stype)

extern fun send {s:stype} {a:vt@ype} (!channel (psend (a) :: s) >> channel (s), a): void
extern fun recv {s:stype} {a:vt@ype} (!channel (precv (a) :: s) >> channel (s)): a
extern fun close (channel (pclose)): void
extern fun wait  (channel (pwait)): void

stadef proto_srv = precv (int) :: precv (int) :: psend (bool) :: pwait
stadef proto_cli = psend (int) :: psend (int) :: precv (bool) :: pclose 

extern fun srv (channel (proto_srv)): void 
extern fun cli (channel (proto_cli)): void 

implement srv (ch) = let 
    val a = recv ch
    val b = recv ch 
    val _ = send (ch, a = b)
in 
    wait ch
end 

implement cli (ch) = let 
    val _ = $showtype ch
    val _ = send (ch, 1)
    val _ = $showtype ch
    val _ = send (ch, 2)
    val _ = $showtype ch
    val b = recv (ch)
    val _ = $showtype ch
in 
    close ch;
end