1 theory Sort_ops

     2 imports Main

     3 begin

     4 

     5 ML {*

     6 local 

     7   open Array

     8 in

     9 

    10  fun swap i j a = let val ai = sub(a, i);

    11                        val _ = update(a, i, sub(a, j))

    12                        val _ = update(a, j, ai)

    13                    in

    14                         a

    15                    end

    16 

    17   fun pre_ops_of a = 

    18    getM :|-- (fn (l, r, piv, i, j) => let

    19        (* val _ = Output.tracing ("("^string_of_int i^","^string_of_int j^")") *)

    20     in

    21     if (j < i) then (returnM (swap l j a) |-- returnM [(l, j)])

    22     else (if (sub(a, i) <= piv andalso i <= r) then (setM (l, r, piv, i + 1, j)

    23                                                         |-- pre_ops_of a)

    24           else if (sub(a, j) > piv ) then (setM (l, r, piv, i, j - 1) |-- pre_ops_of a)

    25           else (pre_ops_of (swap i j a) :|-- (fn ops => returnM ((i,j)::ops))))

    26     end  

    27    )

    28 

    29   fun ops_of i j a = 

    30      if (j < i) then []

    31   else let

    32      val piv = sub(a, i)

    33      val (ops1, (_, _, _, i', j')) = pre_ops_of a (i, j, piv, i, j) |> normVal

    34      val ops2 = ops_of i (j' - 1) a

    35      val ops3 = ops_of (j' + 1) j a

    36   in

    37      ops1 @ ops2 @ ops3 

    38   end

    39 

    40   fun rem_sdup [] = []

    41     | rem_sdup [c] = [c]

    42     | rem_sdup ((i, j)::(i', j')::xs) = if ((i = i' andalso j = j') orelse

    43                                             (i = j' andalso j = i')) then rem_sdup (xs)

    44                             else (i, j)::rem_sdup ((i', j')::xs)

    45   fun sexec [] a = a

    46    | sexec ((i, j)::ops) a = sexec ops (swap i j a)

    47 

    48   fun swaps_of (l:int list) = 

    49     ops_of 0 (List.length l - 1) (fromList l) |> rem_sdup

    50       |> filter (fn (i, j) => i <> j)

    51 end

    52 

    53 *}

    54 

    55 text {* Examples *}

    56 

    57 ML {*

    58   val l = [8, 9, 10, 1, 12, 13, 14] 

    59   val ops = (swaps_of l)

    60   val a = (sexec ops (Array.fromList l))

    61   val l' = Array.vector a

    62   val a = sexec (rev ops) a

    63 *}

    64 

    65 end