val N:ℕ;
val M:ℕ; 

type int   = ℤ[-1,N];
type elem  = ℕ[M];
type array = Array[N,elem];

// we construct from array "a" a new array as follows: we rotate
// the first "n" elements "r" positions to the left (inserting
// the first "r" elements back at the end of the first "n" positions).
// the elements at positions greater equal "n" remain unchanged.
proc rotateLeft(a:array,n:int,r:int): array
{
  var b:array = a;
  var i:int ≔ 0;
  while i < n-r do
  {
    b[i] ≔ a[i+r];
    i = i+1;
  }  
  while i < n do
  {
    b[i] ≔ a[i-n+r];
    i ≔ i+1;
  }
  return b;
}