(*
 * This is an example showing that no array bounds checking
 * is needed in binary search
 *)

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

datatype 'a answer = NONE | SOME of int * 'a

assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a
assert length  <| {n:nat} 'a array(n) -> int(n)

fun('a){size:nat}
bsearch cmp (key, arr) =
let
    fun look(lo, hi) =
	if hi >= lo then
	    let
		val m = (hi + lo) div 2
		val x = sub(arr, m)
	    in
		case cmp(key, x) of
		    LESS => look(lo, m-1)
		  | EQUAL => (SOME(m, x))
		  | GREATER => look(m+1, hi)
	    end
	else NONE
    where look <|
    {l:nat, h:int | 0 <= l <= size /\ 0 <= h+1 <= size } int(l) * int(h) -> 'a answer
in
    look (0, length arr - 1)
end
where bsearch <| ('a * 'a -> order) -> 'a * 'a array(size) -> 'a answer