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:

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]

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] *)

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