mergesort_list: generic code, a bit of cleaning up

examples/mergesort_list.mlw

 
 (* Sorting a list of integers using mergesort *)
 
-module M
+module Elt
 
-  use import int.Int
-  use import list.Length
-  use import list.SortedInt
-  use import list.Append
-  use import list.Permut
+  use export int.Int
+  use export list.Length
+  use export list.Append
+  use export list.Permut
 
-  let split (l0 : list 'a)
+  type elt
+  predicate le elt elt
+  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone export list.Sorted      with type t = elt, predicate le  = le
+
+end
+
+module Merge
+
+  use export Elt
+
+  let rec merge (l1 l2: list elt) : list elt
+    requires { sorted l1 /\ sorted l2 }
+    ensures  { sorted result /\ permut result (l1 ++ l2) }
+    variant  { length l1 + length l2 }
+  = match l1, l2 with
+    | Nil, _ -> l2
+    | _, Nil -> l1
+    | Cons x1 r1, Cons x2 r2 ->
+       if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
+    end
+
+end
+
+(* TODO: proof to be completed
+module EfficientMerge
+
+  use export Elt
+  use import list.Mem
+  use import list.Reverse
+  use import list.RevAppend
+
+  let rec merge_aux (acc l1 l2: list elt) : list elt
+    requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 }
+    requires { forall x y: elt. mem x acc -> mem y l1 -> le x y }
+    requires { forall x y: elt. mem x acc -> mem y l2 -> le x y }
+    ensures  { sorted result /\ permut result (acc ++ l1 ++ l2) }
+    variant  { length l1 + length l2 }
+  = match l1, l2 with
+    | Nil, _ -> rev_append acc l2
+    | _, Nil -> rev_append acc l1
+    | Cons x1 r1, Cons x2 r2 ->
+       if le x1 x2 then merge_aux (Cons x1 acc) r1 l2
+                   else merge_aux (Cons x2 acc) l1 r2
+    end
+
+  let merge (l1 l2: list elt) : list elt
+    requires { sorted l1 /\ sorted l2 }
+    ensures  { sorted result /\ permut result (l1 ++ l2) }
+  =
+    merge_aux Nil l1 l2
+
+end
+*)
+
+module Mergesort
+
+  use import Merge
+
+  let split (l0: list 'a) : (list 'a, list 'a)
     requires { length l0 >= 2 }
-    ensures { let (l1, l2) = result in
+    ensures  { let (l1, l2) = result in
       1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) }
-  = let rec split_aux (l1 : list 'a) l2 l variant { length l }
+  = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a)
       requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
-      ensures { let r1, r2 = result in
+      ensures  { let r1, r2 = result in
         (length r2 = length r1 \/ length r2 = length r1 + 1) /\
         permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
+      variant { length l }
     = match l with
       | Nil -> (l1, l2)
       | Cons x r -> split_aux l2 (Cons x l1) r
@@ -25,18 +84,9 @@ module M
     in
     split_aux Nil Nil l0
 
-  let rec merge l1 l2 variant { length l1 + length l2 }
-    requires { sorted l1 /\ sorted l2 }
-    ensures { sorted result /\ permut result (l1 ++ l2) }
-  = match l1, l2 with
-    | Nil, _ -> l2
-    | _, Nil -> l1
-    | Cons x1 r1, Cons x2 r2 ->
-       if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
-    end
-
-  let rec mergesort l variant { length l }
+  let rec mergesort (l: list elt) : list elt
     ensures { sorted result /\ permut result l }
+    variant { length l }
   = match l with
       | Nil | Cons _ Nil -> l
       | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)