Mergesort on lists

module MergeSortList

  use import int.Int
  use import list.List
  use import list.Length
  use import list.SortedInt
  use import list.Append
  use import list.Permut

 let rec split (l : list int)
 ensures { let (l1, l2) = result in permut l (l1 ++ l2)}
  = match l with
    | Nil -> (Nil, Nil)
    | Cons x Nil -> ((Cons x Nil) , Nil)
    | Cons x (Cons y l') -> let (xs, ys) = split l' in ((Cons x xs), (Cons y ys))
    end

 let rec merge l1 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
 ensures { sorted result }
  = match l with
    | Nil | Cons _ Nil -> l
    | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
    end

end