(* This example shows that there is no need for
   array bounds checking for the QUEEN problem *)

(* 9 type annotations, which occupy 9 lines *)

structure Queen =
    struct
	assert sub <| {size:nat, i:nat | i < size } int array(size) * int(i) -> int
        and update <| {size:nat, i:nat | i < size } int array(size) * int(i) * int -> unit

	fun{size}
	    queen(size) =
	    let
		val queenArray = array(size, 0)
		    
		fun item(i) = sub(queenArray, i)
		where item <| {i:nat | i < size} int(i) -> int

		fun assign(i, j) = update(queenArray, i, j)
		where assign <| {i:nat | i < size} int(i) * int -> unit

		fun dotsPrint(n) = if n = 0 then () else (print "."; dotsPrint(n-1))
                where dotsPrint <| int  -> unit
			
		fun queenPrint() =
		    let
			fun aux(row) =
			    if row = size then ()
			    else
				let
				    val n = item(row)
				in
				    dotsPrint(n-1); print "Q"; dotsPrint(size - n);
				    print"\n"; aux(row + 1)
				end
                        where aux <| {i:nat | i <= size } int(i) -> unit
		    in
			aux(0); print"\n"
		    end
                    where queenPrint <| unit -> unit
		
		fun test(j) =
		    let
			val qj = item j
			fun aux(i) =
			    if (i < j) then
				let
				    val qi = item i
				in
				    if qi = qj then false
				    else if abs(qj - qi) = j - i then false
					 else aux(i+1)
				end
			    else true
                        where aux <| {i:nat | i < size} int(i) -> bool
		    in
			aux(0)
		    end
                 where test <| {j: nat | j < size} int(j) -> bool

		
		fun loop(row) =

		    let
			val next = item(row) + 1
		    in
			if next > size then
			    (assign(row, 0); if (row = 0) then () else loop(row-1))
			else (assign(row, next);
			      if test(row) then
				  if row+1 = size then (queenPrint(); loop(row))
				  else loop(row+1)
			      else loop(row))
		    end

                where loop <| {row:nat | row < size} int(row) -> unit
	    in
		loop(0)
	    end
	    where queen <| {dummy | size > 0} int(size) -> unit
    end