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'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.
(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))))
(defun halve-list (x) (declare (xargs :guard t)) (halve-list-aux x x nil))