(* IMPERATIVE *)
open Array;

fun printarray A =
    let val n = length A;
	val i = ref 0;
    in  ( print ("         [");
          while (!i < n) do
          (  print (Int.toString (sub (A, !i)));
	     if (!i < n-1) then print (",") else (); 
             i := !i +1
          );
          print ("]\n")
	)
    end;

(*
## Assume A0 is the initial value of the array A[0..n-1]
## ordered (A, p, q) = forall j: 0 <= p <= j < q < n -> A[j] <= A[j+1]
## leftmin (A, p ) = forall i: 0 <= i < p < n: forall j: p <= j< n: A[i] <= A[j]
*)

fun swap (A, i, j) = 
    let val temp = sub (A, i)
    in (update (A, i, sub (A, j));
        update (A, j, temp)
       )
    end;
    
local
     fun findIndexOfMin (A, i, n) =
	 let val m = ref i and k = ref i
	     (* 
	        INV2: 0<= i <= !m <= !k /\ 
                       forall j: 0<= i<=j < k <= n: A[m] <= A[j]
	     *)
	 in while !k < n do
                  (
                    if sub (A, !k) < sub (A, !m)
		    then m := !k 
                    else ();
		    k := !k + 1
		  );
                  !m
	 end

in fun selSortImp A =
   let 
     val n = length A; (* A[0..n-1] *)
     val p = ref 0;
     val q = ref 0;

    (* 
       ordered (A, i, k) = forall j: 0 <= i <= j < k < n-1: A[j] <= A[j+1]
       leftmin (A, p) = forall i, j: 0 <= i < p <= j < n: A[i] <= A[j]

       INV1: perm (A, A0) & 0<=p<=n & ordered (A, 0, p) & leftmin (A, p) 

       BF : n-p
    *)
    in (  
          while !p < n do
          (
             q := findIndexOfMin (A, !p, n); 
             swap (A, !q, !p);
	     p := !p + 1
          ); (* the algo terminates once !p = n *)
          printarray A
       )
   end
end;

val si = selSortImp;
si (fromList [~12, ~24, ~12, 0, 123, 45, 1, 20, 0, ~24]);