(* This simple example shows that bubble
 * sort needs no array bounds checking *)

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

structure BubbleSort =
    struct	
	assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a
        and    update <| {n:nat, i:nat| i < n } 'a array(n) * int(i) * 'a -> unit
        and    length <| {n:nat} 'a array(n) -> int(n)

	fun('a){size:nat}
	    bubbleSort cmp arr =
	    let
		val size = length(arr)
		fun item(i) = sub(arr, i)
		where item <| {i:nat | i < size } int(i) -> 'a

		fun loop(i, j) =
		    if j = 0 then ()
		    else if (i = j) then loop(0, j-1)
			 else
			     case cmp(item(i), item(i+1)) of
				 GREATER =>
				     let
					 val temp = item(i)
				     in
					 update(arr, i, item(i+1));
					 update(arr, i+1, temp);
					 loop(i+1, j)
				     end
			       | _ => loop(i+1, j)
                where loop <| {i:nat, j:nat | i <= j < size } int(i) * int(j) -> unit
	    in
		if size <= 1 then () else loop(0, size - 1)
	    end	
         where bubbleSort <| ('a * 'a -> order) -> 'a array(size) -> unit
    end