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