(* 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