		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Mergesort-jmethods

Sort a list of methods according to their names.

Signature
(mergesort-jmethods methods) → sorted-methods
Arguments: methods — Guard (jmethod-listp methods).
Returns: sorted-methods — Type (jmethod-listp sorted-methods), given the guard.

Definitions and Theorems

Function: merge-jmethods

(defun merge-jmethods (methods1 methods2)
  (declare (xargs :guard (and (jmethod-listp methods1)
                              (jmethod-listp methods2))))
  (let ((__function__ 'merge-jmethods))
    (declare (ignorable __function__))
    (cond ((endp methods1) methods2)
          ((endp methods2) methods1)
          (t (if (string<= (jmethod->name (car methods1))
                           (jmethod->name (car methods2)))
                 (cons (car methods1)
                       (merge-jmethods (cdr methods1)
                                       methods2))
               (cons (car methods2)
                     (merge-jmethods methods1 (cdr methods2))))))))

Theorem: jmethod-listp-of-merge-jmethods

(defthm jmethod-listp-of-merge-jmethods
  (implies (and (jmethod-listp methods1)
                (jmethod-listp methods2))
           (b* ((merged-methods (merge-jmethods methods1 methods2)))
             (jmethod-listp merged-methods)))
  :rule-classes :rewrite)

Function: mergesort-jmethods

(defun mergesort-jmethods (methods)
  (declare (xargs :guard (jmethod-listp methods)))
  (let ((__function__ 'mergesort-jmethods))
    (declare (ignorable __function__))
    (b* ((len-methods (len methods))
         ((when (<= len-methods 1)) methods)
         (len/2 (floor len-methods 2))
         (methods1 (mergesort-jmethods (take len/2 methods)))
         (methods2 (mergesort-jmethods (nthcdr len/2 methods))))
      (merge-jmethods methods1 methods2))))

Theorem: jmethod-listp-of-mergesort-jmethods

(defthm jmethod-listp-of-mergesort-jmethods
  (implies (and (jmethod-listp methods))
           (b* ((sorted-methods (mergesort-jmethods methods)))
             (jmethod-listp sorted-methods)))
  :rule-classes :rewrite)