# Halve-list

How we split the list for mergesort.

Originally I used the following function to split the list.

(defun split-list-old (x)
(declare (xargs :guard (true-listp x)))
(cond ((endp x) (mv nil nil))
((endp (cdr x)) (mv (list (car x)) nil))
(t (mv-let (part1 part2)
(split-list-old (cddr x))
(mv (cons (car x) part1)
(cons (cadr x) part2)))))))

But David Rager noted that this was not tail recursive, and accordingly it
ran into trouble on large data sets. Accordingly, in Version 0.91, I rewrote
this to be tail recursive:

(defun split-list (x acc acc2)
(declare (xargs :guard (true-listp x)))
(cond ((endp x)
(mv acc acc2))
((endp (cdr x))
(mv (cons (car x) acc) acc2))
(t (split-list (cddr x)
(cons (car x) acc)
(cons (cadr x) acc2)))))

Since then, I wrote the defsort/defsort library, which uses some tricks
to provide a faster mergesort. One key optimization is to take the first and
second halves of the list, rather than splitting the list in terms of evens and
odds. This allows you to split the list with half as much consing.

Defsort's approach uses a lot of arithmetic optimization. I later wrote a
mergesort for Milawa, where arithmetic is expensive. Here, I implemented
split-list by walking down "one cdr" and "two cdrs" at a time. I now use
this same strategy in osets.

BOZO this strategy is still stupidly re-consing up half the list, when
really we could avoid that by just being a bit smarter, like in defsort.

### Definitions and Theorems

**Function: **halve-list-aux

(defun halve-list-aux (mid x acc)
(declare (xargs :guard (<= (len x) (len mid))))
(if (or (atom x) (atom (cdr x)))
(mv acc mid)
(halve-list-aux (cdr mid)
(cdr (cdr x))
(cons (car mid) acc))))

**Function: **halve-list

(defun halve-list (x)
(declare (xargs :guard t))
(halve-list-aux x x nil))