open Interpret

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

type bool =
  | True
  | False

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

let fst = function
  | Pair (x, y) -> x

let snd = function
  | 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)), ZeroP)))

let client i o =
  NuPl (fun r -> ParP ((OutP (True, i, (Pair (O, r)), ZeroP)), (InP
    (True, r, (fun x -> OutP (False, o, x, ZeroP))))))

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

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


main ();;