theory Sort_ops+
−
imports Term_pat+
−
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+
−