		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Mergesort-jfields

Sort a list of fields according to their names.

Signature
(mergesort-jfields fields) → sorted-fields
Arguments: fields — Guard (jfield-listp fields).
Returns: sorted-fields — Type (jfield-listp sorted-fields), given the guard.

Definitions and Theorems

Function: merge-jfields

(defun merge-jfields (fields1 fields2)
  (declare (xargs :guard (and (jfield-listp fields1)
                              (jfield-listp fields2))))
  (let ((__function__ 'merge-jfields))
    (declare (ignorable __function__))
    (cond ((endp fields1) fields2)
          ((endp fields2) fields1)
          (t (if (string<= (jfield->name (car fields1))
                           (jfield->name (car fields2)))
                 (cons (car fields1)
                       (merge-jfields (cdr fields1) fields2))
               (cons (car fields2)
                     (merge-jfields fields1 (cdr fields2))))))))

Theorem: jfield-listp-of-merge-jfields

(defthm jfield-listp-of-merge-jfields
  (implies (and (jfield-listp fields1)
                (jfield-listp fields2))
           (b* ((merged-fields (merge-jfields fields1 fields2)))
             (jfield-listp merged-fields)))
  :rule-classes :rewrite)

Function: mergesort-jfields

(defun mergesort-jfields (fields)
  (declare (xargs :guard (jfield-listp fields)))
  (let ((__function__ 'mergesort-jfields))
    (declare (ignorable __function__))
    (b* ((len-fields (len fields))
         ((when (<= len-fields 1)) fields)
         (len/2 (floor len-fields 2))
         (fields1 (mergesort-jfields (take len/2 fields)))
         (fields2 (mergesort-jfields (nthcdr len/2 fields))))
      (merge-jfields fields1 fields2))))

Theorem: jfield-listp-of-mergesort-jfields

(defthm jfield-listp-of-mergesort-jfields
  (implies (and (jfield-listp fields))
           (b* ((sorted-fields (mergesort-jfields fields)))
             (jfield-listp sorted-fields)))
  :rule-classes :rewrite)