(*
 * This example shows that no array bounds checking
 * is needed for array multiplication.
 *)

(* 5 type annotations, which occupy about 10 lines *)

structure Array2D =
    struct 
	
	type 'a array2D = {m:nat, n:nat} int(m) * int(n) * 'a array(m * n)
	    
	assert sub <|  'a array * int -> 'a (* safe version *)
	and    update <| 'a array * int * 'a -> unit (* safe version *)

	fun('a)
	 sub2D((m, n, arr), i, j) = sub(arr, m * i + j)
        where sub2D <|
	{m:nat, n:nat, i:nat, j:nat | i < m /\ j < n}
	'a array2D(m,n) * int(i) * int(j) -> 'a

	fun('a)
	 update2D((m, n, arr), i, j, v) = update(arr, m * i + j, v)
	where update2D <|
	{m:nat, n:nat, i:nat, j:nat | i < m /\ j < n}
	'a array2D(m,n) * int(i) * int(j) * 'a -> unit


	fun{l:nat, m:nat, n:nat}
	    arrayMult(arr2D1 as (l1, m1, arr1),
		      arr2D2 as (m2, n2, arr2),
		      arr2D3 as (l3, n3, arr3)) =
	    let
		fun loop(i, j, k, sum) =
		    if (k = m1) then sum
		    else loop(i, j, k+1, sum + sub2D(arr2D1, i, k) * sub2D(arr2D2, k, j))
		where loop <|
		{i: nat, j:nat, k:nat | i < l /\ j < n /\ k <= m}
		int(i) * int(j) * int(k) * int -> int
			
		fun aux(i, j) =
		    if (i = l1) then ()
		    else if (j = n2) then aux(i+1, 0)
			 else (update2D(arr2D3, i, j, loop(i, j, 0, 0)); aux(i, j+1))
		    where aux <| {i: nat, j:nat | i <= l /\ j <= n } int(i) * int(j) -> unit
	    in
		aux(0, 0)
	    end
	where arrayMult <| int array2D(l, m) * int array2D(m, n) * int array2D(l, n) -> unit
    end