		Search-engine friendly clone of the ACL2 documentation.

Utilities

Redundant-mergesort

Same as mergesort, but avoids re-sorting lists that are already sorted.

Signature
(redundant-mergesort x &key warnp from) → *
Arguments: warnp — print warnings when x is not sorted?.
Guard (booleanp warnp).; from — context to help track down warnings.
Guard (symbolp from).

In the logic, (redundant-mergesort x) is just (mergesort x). But in the execution, it first checks to see if x is already sorted, and if so returns x unchanged.

I use this function when I do not want to go to the trouble of proving that some cons-based operation happens to produce a set. In practice, this should be much faster than a mergesort because checking (setp x) is linear and requires no consing.

By default, redundant-mergesort is silent and will simply sort its argument if necessary. However, you can also instruct it to emit warnings. A typical example is:

(defun my-function (x)
   (let ((x-sort (redundant-mergesort x :warnp t :from 'my-function)))
      ...))

Definitions and Theorems

Function: redundant-mergesort-fn

(defun
 redundant-mergesort-fn (x warnp from)
 (declare (xargs :guard (and (booleanp warnp) (symbolp from))))
 (let
  ((__function__ 'redundant-mergesort))
  (declare (ignorable __function__))
  (mbe
   :logic (mergesort x)
   :exec
   (if
    (setp x)
    x
    (prog2$
     (cond
         ((and warnp from)
          (cw "; Redundant-mergesort given unsorted list by ~s0.~%"
              from))
         (warnp (cw "; Redundant-mergesort given unsorted list.~%"))
         (t nil))
     (mergesort x))))))