mergesort_list.mlw 1.29 KB
Newer Older
1 2 3

(* Sorting a list of integers using mergesort *)

4
module M
5

6
  use import int.Int
7
  use import list.Length
8
  use import list.SortedInt
9 10 11
  use import list.Append
  use import list.Permut

12 13 14 15 16 17 18 19 20 21
  let split (l0 : list 'a)
    requires { length l0 >= 2 }
    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 }
      requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
      ensures { let r1, r2 = result in
        (length r2 = length r1 \/ length r2 = length r1 + 1) /\
        permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
    = match l with
22 23 24 25 26
      | Nil -> (l1, l2)
      | Cons x r -> split_aux l2 (Cons x l1) r
      end
    in
    split_aux Nil Nil l0
27

28 29 30 31
  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
32 33 34 35 36
    | 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
37

38 39 40
  let rec mergesort l variant { length l }
    ensures { sorted result /\ permut result l }
  = match l with
41 42
      | Nil | Cons _ Nil -> l
      | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
43 44
    end

45
end