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