open Interpret;;

(************************ code generated by Coq ***************************)

type bool = True | False;;

type ('a, 'b) prod = Pair of 'a * 'b;;

let fst = fun (Pair (x, y)) -> x;;

let snd = fun (Pair (x, y)) -> y;;

type nat = O | S of nat;;

let rec plus n m =
  match n with
    O -> m
  | S p -> S (plus p m)
;;

let server i =
  rinP
    (true, i,
     (fun ar -> outP (true, snd ar, plus (fst ar) (S O), (fun _ -> zeroP))))
;;

let client i o =
  nuPl
    (fun r ->
       parP
         (outP (true, i, Pair (O, r), (fun _ -> zeroP)),
          inP (true, r, (fun x -> outP (false, o, x, (fun _ -> zeroP))))))
;;

(****************************** entry point ***************************)

let main () =
  let i = new channel in let o = new channel in parP (server i, client i o)
;;


main ();;