--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Sort_ops.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,65 @@
+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
\ No newline at end of file