I present a standard implementation of insertion sort on linear lists in this section. The interface for insertion sort is given as follows:

fun{ a:t@ype } insertionSort{n:nat} (xs: list_vt (a, n), cmp: cmp a): list_vt (a, n) // end of [insertionSort]

The following code implements a function insord that inserts a given list-node into a sorted linear list to form another sorted linear list:

fun{ a:t@ype } insord {l0,l1,l2:addr}{n:nat} ( pf1: a @ l1 , pf2: list_vt (a, 0)? @ l2 | xs0: &list_vt (a, n) >> list_vt (a, n+1) , nx0: list_vt_cons_unfold (l0, l1, l2), p1: ptr (l1), p2: ptr (l2) , cmp: cmp (a) ) : void = ( case+ xs0 of | @list_vt_cons (x0, xs1) => let val sgn = compare<a> (x0, !p1, cmp) in if sgn <= 0 // HX: for stableness: [<=] instead of [<] then let val () = insord<a> (pf1, pf2 | xs1, nx0, p1, p2, cmp) prval () = fold@ (xs0) in // nothing end // end of [then] else let prval () = fold@ (xs0) val () = (!p2 := xs0; xs0 := nx0) prval () = fold@ (xs0) in // nothing end // end of [else] // end of [if] end // end of [list_vt_cons] | ~list_vt_nil () => { val () = xs0 := nx0 val () = !p2 := list_vt_nil () prval () = fold@ (xs0) } ) (* end of [insord] *)

The function template insertionSort can now be readily implemented based insord:

implement{a} insertionSort (xs, cmp) = let // fun loop{m,n:nat} ( xs: list_vt (a, m) , ys: &list_vt (a, n) >> list_vt (a, m+n) , cmp: cmp (a) ) : void = case+ xs of | @list_vt_cons (x, xs1) => let val xs1_ = xs1 val ((*void*)) = insord<a> (view@x, view@xs1 | ys, xs, addr@x, addr@xs1, cmp) // end of [va] in loop (xs1_, ys, cmp) end // end of [list_vt_cons] | ~list_vt_nil ((*void*)) => () // var ys = list_vt_nil{a}() val () = loop (xs, ys, cmp) // in ys end // end of [insertionSort]

fun{ a:t@ype } msort{n:nat} .<n>. ( xs: list_vt (a, n) , n: int n, cmp: cmp(a) ) : list_vt (a, n) = let // // cutoff is selected to be 10 // in if n > 10 then let val n2 = half(n) val n3 = n - n2 var xs = xs // lvalue for [xs] val ys = split<a> (xs, n3) val xs = msort<a> (xs, n3, cmp) val ys = msort<a> (ys, n2, cmp) var res: List_vt (a) // uninitialized val () = merge<a> (xs, ys, res(*cbr*), cmp) in res end else insertionSort<a> (xs, cmp) end // end of [msort]

Please find the entire code in this section plus some additional code for testing on-line.