01_send_receive.clc

typedefs
  Bool = 1 + 1 ;
  Nat  = rec X : *ns. 1 + X ;

  Cliente  = !Nat.?Bool.End ;
  Servidor = ?Nat.!Bool.End
end

let un false : Bool = inl [1] {} in
let un true  : Bool = inr [1] {} in

let un zero : Nat = fold [Nat] (inl [Nat] {}) in

let rec discardNat : Nat -o 1 =
  \lin n : Nat.
    case unfold n of
      inl u ->
        u ;

      inr m ->
        discardNat m
in

let un isZero : Nat -o Bool =
  \lin n : Nat.
    case unfold n of
      inl u ->
        let {} = u in
        true ;

      inr m ->
        let {} = discardNat m in
        false
in

-------------------------------------------------------

let un cliente : Cliente -o Bool =
  \lin c0 : Cliente.
    let lin c1  = send zero c0 in
    let {b, c2} = receive c1   in
    let {}      = close c2     in
    b
in

let un servidor : Servidor -o 1 =
  \lin s0 : Servidor.
    let {n, s1} = receive s0         in
    let lin s2  = send (isZero n) s1 in
    close s2
in

let lin c = fork servidor in
cliente c