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