let{size:int | size > 0}
play size =
  let leftPost = make_vect size 0
  and middlePost = make_vect size 0
  and rightPost = make_vect size 0 in

  let initialize post =
    for i = 0 to size - 1 do
      post..(i) <- i+1
    done
  withtype int vect(size) -> unit in

  let showpiece n =
    for i = 1 to n do print_string "O" done;
    for i = n + 1 to size do print_string " " done in

  let showposts () =
    for i = 0 to size - 1 do
      showpiece leftPost..(i);
      print_string "  ";
      showpiece middlePost..(i);
      print_string "  ";
      showpiece rightPost..(i);
      print_newline ()
    done;
    print_newline ()
  withtype unit -> unit in

  let _ = initialize(leftPost) in
  let rec move (n, source, s, post, p, post', p') =
    if eq_int n 1 then
      begin post..(p - 1) <- source..(s); source..(s) <- 0; showposts() end
    else begin
      move(n-1, source, s, post', p', post, p);
      post..(p - 1) <- source..(s + n - 1);
      source..(s + n - 1) <- 0;
      showposts ();
      move(n-1, post', p'-n+1, post, p - 1, source, s + n)
    end
  withtype {n:nat}{s:nat}{p:nat}{p':nat |
            p <= size /\ p' <= size /\ s + p + p' = size + size /\ 0 < n /\
            s + n <= size /\ n <= p /\ n <= p' }
           int(n) * int vect(size) * int(s) * int vect(size) * int(p) * int vect(size) * int(p') -> unit in
  showposts();
  move(size, leftPost, 0, rightPost, size, middlePost, size)
withtype int(size) -> unit
;;