Example: Ordering Permutations

Given a natural number n, we want to print out all the permutations consisting of integers ranging from 1 to n, inclusive. In addition, we want to print them out according to the lexicographic ordering on integer sequences. For instance, we want the following output to be generated when n is 3:

1, 2, 3
1, 3, 2
2, 1, 3
2, 3, 1
3, 1, 2
3, 2, 1

Let us first define a function as follows for printing out an array of integers:

fun print_intarray (A: arrszref(int)): void = loop(0, ", ") where { // val asz = g0uint2int_size_int(A.size()) // // The integers are to be separated by the string [sep] // fun loop (i: int, sep: string): void = if i < asz then (if i > 0 then print sep; print A[i]; loop(i+1, sep)) // end of [if] } (* end of [print_intarray] *)

We next implement two functions lrotate and rrotate for rearranging the elements in a given integer array:

fun lrotate ( A: arrszref int, i: int, j: int ) : void = let fun lshift ( A: arrszref int, i: int, j: int ) : void = if i < j then (A[i] := A[i+1]; lshift(A, i+1, j)) // end of [if] in if i < j then let val tmp = A[i] in lshift(A, i, j); A[j] := tmp end // end of [if] end // end of [lrotate] fun rrotate ( A: arrszref int, i: int, j: int ) : void = let fun rshift ( A: arrszref int, i: int, j: int ) : void = if i < j then (A[j] := A[j-1]; rshift(A, i, j-1)) // end of [if] in if i < j then let val tmp = A[j] in rshift(A, i, j); A[i] := tmp end // end of [if] end // end of [rrotate]

When applied to an array and two valid indexes i and j for the array such that i is less than or equal to j, lrotate moves simultaneously the content of cell i into cell j and the content of cell k to cell k-1 for k ranging from i+1 to j, inclusive. The function rrotate is similar to lrotate but shuffles elements in the opposite direction.

Given a natural number n, the following defined function permute prints out all the permutations consisting of integers ranging from 1 to n, inclusive while arranging the output according to the lexicographic ordering on integer sequences.

fun permute ( n: int ) : void = aux(1) where { // #define i2sz g0int2uint_int_size // // Creating array A of size n // val A = arrszref_make_elt<int>(i2sz(n), 0) // // Initializing A // with integers from 1 to n, inclusive // val () = init(0) where { fun init(i: int): void = if i < n then (A[i] := i+1; init(i+1)) // end of [if] } // end of [where] // end of [val] // fun aux (i: int): void = ( if i <= n then aux2(i, i) else ( print_intarray(A); print_newline() ) (* end of [else] *) ) (* end of [aux] *) // and aux2 (i: int, j: int): void = ( if j <= n then let val () = ( rrotate(A, i-1, j-1); aux(i+1); lrotate(A, i-1, j-1) ) // end of [val] in aux2 (i, j + 1) end // end of [if] ) (* end of [aux2] *) // } (* end of [permute] *)

Note that where is a keyword, and the expression (exp where { decseq }) for some expression exp and declaration sequence decseq is equivalent to the let-expression of the form (let decseq in exp end). To understand the behavior of the function aux, let us evaluate aux(1) while assuming that n is 4 and the 4 elements of the array A are 1, 2, 3, and 4. It should be fairly straightforward to see that this evaluation leads to the evaluation of aux(2) for 4 times: the array A contains (1, 2, 3, 4) for the first time, and (2, 1, 3, 4) for the second time, and (3, 1, 2, 4) for the third time, and (4, 1, 2, 3) for the fourth time. With some inductive reasoning, it should not be difficult to see that evaluating aux(1) indeed leads to all the permutations being output according to the lexicographic ordering on integer sequences.

Please find the entire code in this section plus some additional code for testing on-line.