Verbs in Action

Written by: Hongwei Xi (the creator of ATS)

Let's see some verbs in action!

The famous 8-queen puzzle asks the player to find ways to put eight queen pieces on a chess board such that no queen piece can attack any other ones. In other words, no two queen pieces can be put on the same row, the same column, or the same diagnal.

Let us first declare an abstract type board for values representing board configurations and then implement it as a list:

(* ****** ****** *)

abstbox board = ptr

(* ****** ****** *)

extern
fun
board_nil(): board
and
board_cons(int, board): board

(* ****** ****** *)

local

absimpl board = list0(int)

in(* in-of-local *)

implement
board_nil() = nil()
implement
board_cons(x0, xs) = cons(x0, xs)

implement
gseq_streamize<board><int>(xs) = list0_streamize<int>(xs)

end (* end of [local] *)

Note that the verb streamize is implemented for board, which immidiately makes all of the other verbs listed above available for use.

For instance, the following function board_check can be called to check if putting a queen piece at column x0 on the next row can cause a conflict with the queen pieces on the current board xs:

fun
board_check
(x0: int, xs: board): bool =
(
gseq_iforall<board><int>(xs)
) where
{
implement
gseq_iforall$test<int>(i1, x1) =
if (x0 != x1) then (abs(x0 - x1) != i1 + 1) else false
}

Note that abs stands for the absolute value function. The next function board_print is for printing out a given board:

fun
board_print
(xs: board): void =
(
gseq_rforeach<board><int>
  (xs)
) where
{
implement
gseq_rforeach$work<int>(x0) =
(
  loop(0)
) where
{
fun
loop(i0: int): void =
if
i0 >= N
then
println!((*void*))
else
(
if i0 = x0 then print "Q " else print ". "; loop(i0+1)
)
}
} (* end of [board_print *)

Note that the verb rforeach is used because the list representation of a board actually represents the board in the reverse order: the first element in the list represents the column position of the last queen piece and the last element in the list represents the column position of the first queen piece. For instance, Solution#1 is printed out as follows:

Solution#1:
Q . . . . . . . 
. . . . Q . . . 
. . . . . . . Q 
. . . . . Q . . 
. . Q . . . . . 
. . . . . . Q . 
. Q . . . . . . 
. . . Q . . . . 

Please find the entirety of the implementation here.