unit print_space (n:int) {
  var: nat i;;

  for (i = 0; i < n; i = i + 1) {
    print_string (" ");
  }
}

unit print_disk (size: int, n: int) {
  var: nat i;;

  for (i = 0; i < n; i = i + 1) {
    print_string ("O");
  }
  print_space (size - n);
}

{size:nat}
unit print_posts (size: int(size), posts[3][size]: int) {
  var: nat i;;

  for (i = 0; i < size; i = i + 1) {
    print_disk (size, posts[0][i]); print_string ("\t");
    print_disk (size, posts[1][i]); print_string ("\t");
    print_disk (size, posts[2][i]); print_string ("\n");
  }
}

{size:nat, n:pos, s:nat, d1:int, d2:int |
 d1 <= size, d2 <= size, s+d1+d2=size+size, s+n <= size, n <= d1, n <= d2}
unit move (size: int(size), posts[3][size]: int, n:int(n),
           sp: int[0,3), s: int(s),
           dp1: int[0,3), d1: int(d1),
           dp2: int[0,3), d2: int(d2)) {

  if (n == 1) {
    posts[dp1][d1-1] = posts[sp][s]; posts[sp][s] = 0;
    print_posts (size, posts); print_newline ();
  } else {
    move (size, posts, n-1, sp, s, dp2, d2, dp1, d1);
    posts[dp1][d1-1] = posts[sp][s+n-1];
    posts[sp][s+n-1] = 0;
    print_posts (size, posts); print_newline ();
    move (size, posts, n-1, dp2, d2-n+1, dp1, d1-1, sp, s+n);
  }
}

{n:int | n > 0}
unit play (size: int(n)) {
  var: int posts[3][n]; nat i;;

  posts = alloc (3, alloc (size, 0));
  posts[1] = alloc (size, 0);
  posts[2] = alloc (size, 0);

  for (i = 0; i < size; i = i + 1) {
    posts[0][i] = i + 1;
  }
  print_posts (size, posts); print_newline ();
  move (size, posts, size, 0, 0, 1, size, 2, size);
}

unit main () {
  play (8);
}