(*
 * This example shows that array bounds checking is
 * unnecessary for the insertion sorting on an array
 *)

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

structure InsertQort =
    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}
	    isort(arr, start, n, cmp) =
	    let
		fun item i = sub(arr,i)
		    where item <| {i:nat | i < size } int(i) -> 'a
		    
		fun swap (i,j) =
		    let 
			val tmp = item i
		    in
			update(arr,i, item j); update(arr,j,tmp)
		    end
		where swap <| {i:nat, j:nat | i < size /\ j < size } int(i) * int(j) -> unit
		
		fun vecswap (i,j,n) =
		    if (n = 0) then () else (swap(i,j);vecswap(i+1,j+1,n-1))
		where vecswap <|
		{i:nat, j:nat, n:nat | i+n <= size /\ j+n <= size}
		int(i) * int(j) * int(n) -> unit

		fun insertSort (start, n) =
		    let
			val limit = start+n
			fun outer i =
			    if i >= limit then ()
			    else
				let
				    fun inner j =
					if j <= start
					    then outer(i+1)
					else
					    let
						val j' = j - 1
					    in
						case cmp(item j',item j) of
						    GREATER => (swap(j,j'); inner j')
						  | _  => outer(i+1)
					    end
					where inner <| {j:nat | j < size } int(j) -> unit
				in
				    inner i
				end
			    where outer <| {i:nat} int(i) -> unit
		    in
			outer (start+1)
		    end
		where insertSort <|
		{start:nat, n:nat | start+n <= size } int(start) * int(n) -> unit
	    in
		insertSort (start, n); arr
	    end
	where isort <|
	{start:nat, n:nat | start + n <= size }
	'a array(size) * int(start) * int(n) * ('a * 'a -> order) -> 'a array(size)
			 
	fun('a){size:nat}
	    sorted cmp arr =
	    let
		val len = length arr
		fun s (v,i) =
		    let
			val v' = sub(arr,i)
		    in
			case cmp(v,v') of
			    GREATER => false
			  | _ => if i+1 = len then true else s(v',i+1)
		    end
		where s <| {i:nat | i < size } 'a * int(i) -> bool
	    in
		if len <= 1 then true else s(sub(arr,0),1)
	    end
	where sorted <| ('a * 'a -> order) -> 'a array(size) -> bool

    end