(* Merging and sorting *)

datatype 'a list =
  nil(0) | {n:nat} cons(n+1) of 'a * 'a list(n)
;;

datatype 'a listlist =
  listnil(0) | {m:nat}{n:nat} listcons(m+n) of 'a list(m) * 'a listlist(n)
;;

let rec merge order = fun
    nil l2 -> l2
  | l1 nil -> l1
  | (cons(h1, t1) as l1) (cons(h2, t2) as l2) ->
      if order h1 h2 then cons(h1, merge order t1 l2) else cons(h2, merge order l1 t2)
withtype ('a -> 'a -> bool) -> {m:nat}{n:nat} 'a list(m) -> 'a list(n) -> 'a list(m+n)
;;

(*
This style is not working yet:

let merge order =
  merge_rec where rec merge_rec = fun
    nil l2 -> l2
  | l1 nil -> l1
  | (cons(h1, t1) as l1) (cons(h2, t2) as l2) ->
      if order h1 h2 then cons(h1, merge_rec t1 l2) else cons(h2, merge_rec l1 t2)
  withtype {m:nat}{n:nat} 'a list(m) -> 'a list(n) -> 'a list(m+n)
;;
*)


let sorting order l =
  let rec initlist = function
      nil -> listnil
    | cons(_, nil) as singleton -> listcons(singleton, listnil)
    | cons(e1, cons(e2, rest)) -> (* Notice the type annotation below: a real lesson *)
        listcons((if order e1 e2 then cons(e1, cons(e2, nil)) else cons(e2, cons(e1, nil)) : 'a list(2)),
                 initlist rest)
  withtype {n:nat} 'a list(n) -> 'a listlist(n) in
  let rec merge2 = function
      listcons(l1, listcons(l2, rest)) -> listcons(merge order l1 l2, merge2 rest)
    | listcons(_, listnil) as x -> x
    | listnil as x -> x
  withtype {n:nat} 'a listlist(n) -> 'a listlist(n) in
  let rec mergeall = function
      listnil -> nil
    | listcons(l, listnil) -> l
    | listcons(_, listcons(_, _)) as llist -> mergeall (merge2 llist)
  withtype {n:nat} 'a listlist(n) -> 'a list(n) in
  mergeall(initlist l)
withtype ('a -> 'a -> bool) -> {n:nat} 'a list(n) -> 'a list(n)
;;