Demo Polarized Protocol
12345678910111213141516171819202122232425262728293031323334353637383940
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
Ats
INFO