theory Sort_ops

imports Main

begin

ML {*

local 

  open Array

in

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

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

                       val _ = update(a, j, ai)

                   in

                        a

                   end

  fun pre_ops_of a = 

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

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

    in

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

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

                                                        |-- pre_ops_of a)

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

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

    end  

   )

  fun ops_of i j a = 

     if (j < i) then []

  else let

     val piv = sub(a, i)

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

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

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

  in

     ops1 @ ops2 @ ops3 

  end

  fun rem_sdup [] = []

    | rem_sdup [c] = [c]

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

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

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

  fun sexec [] a = a

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

  fun swaps_of (l:int list) = 

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

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

end

*}

text {* Examples *}

ML {*

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

  val ops = (swaps_of l)

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

  val l' = Array.vector a

  val a = sexec (rev ops) a

*}

end