Filtering...

defsort

books/defsort/defsort

Included Books

generic support
other
(in-package "ACL2")
include-book
(include-book "generic")
include-book
(include-book "std/util/support" :dir :system)
other
(defxdoc defsort
  :parents (std/lists)
  :short "Define a sorting function for a given comparator."
  :long "<h5>NOTE: Defsort's interface has a greater than average likelihood of
changing incompatibly in the future.</h5>

<p>Defsort creates a relatively-high-performance sorting function for a given
comparison function, and proves that its output is an ordered (with respect to
the comparison function) permutation of the input list.  It is currently
implemented as a mergesort on lists with some fixnum optimizations.</p>

<p>It also may optionally prove the generated mergesort function equivalent to
an insertion sort; this requires some extra properties to be proved about the
comparison function beforehand; see the discussion of @(':weak') below.</p>

<h3>Usage</h3>

<p>These forms show various ways of invoking defsort:</p>
@({
  (defsort sort-by-foo<
           :prefix foosort
           :compare< foo<
           :comparablep foo-p
           :comparable-listp foolist-p
           :true-listp nil
           :weak t)

  (defsort :comparablep rationalp
           :compare< <
           :prefix <
           :comparable-listp rational-listp
           :true-listp t
           :weak nil)

  (defsort intalist-sort
           :extra-args (alist)
           :extra-args-guard (intalistp alist)
           :compare< intalist-<
           :comparablep (lambda (x alist) (consp (assoc-equal x alist))))

  (defsort intalist-sort2 (x alist)
           :extra-args-guard (intalistp alist)
           :compare< intalist2-<
           :comparablep (lambda (x alist) (stringp x)))


})

<p>The first form is a new syntax that gives the name of the sorting function
explicitly; it is also good for etags generation since it is of the form
@('(def... name ...)').  In the first form, the prefix is optional; if it is
not provided, the sort name will be used as the prefix for generating other
function names.</p>

<p>The second form shows an older syntax in which the sort name is omitted and
every function name is generated from the prefix, so the name of the sorting
function will in this case be @('<-sort').</p>

<p>The third form shows the use of @(':extra-args') to define a parameterized
sort.</p>

<p>The fourth form shows a different syntax for specifying extra-args by giving
a formals list before the keyword arguments, which looks a bit nicer.  (Note:
In this syntax the first formal must be the symbol X, although it can be in any
package.)  Additionally, it shows how to use extra-args in conjunction with a
comparablep predicate that doesn't use them.</p>

<h4>Keyword Arguments</h4>
<ul>

<li>@(':compare<') gives the function to use to compare elements; this may be a
binary function name or a lambda such as @('(lambda (x y) (< y x))').  Defsort
needs to prove that this is a transitive relation.</li>

<li>@(':prefix') defaults to the sort name when it is provided, but otherwise
is required.  It is used to generate function and theorem names.</li>

<li>@(':comparablep') gives the type of element to be compared.  The comparison
function's guards should be satisfied by any two elements that both satisfy
this predicate.  This may be a unary function symbol or lambda.  If it is
omitted, then it is treated as @('(lambda (x) t)'), i.e. all objects are
comparable.</li>

<li>@(':comparable-listp') gives the name of a function that recognizes a list
of comparable elements.  This may be omitted, in which case such a function
will be defined (named @('<prefix>-list-p')).</li>

<li>@(':true-listp') defaults to NIL and determines whether the
comparable-listp function requires the final cdr to be NIL.  If an existing
@(':comparable-listp') function name is provided, then the value of
@(':true-listp') must correspond to that function; i.e. true-listp must be true
iff the comparable-listp function requires the final cdr to be nil.  If
@(':comparable-listp') is not provided, then the comparable-listp function will
be generated so that this is true.</li>

<li>@(':weak') defaults to NIL in the new syntax and T in the old syntax, for
historical reasons.  When @(':weak') is NIL, defsort will introduce a simple
insertion sort function in addition to the optimized mergesort, and prove the
two equivalent.  To do this, it needs a couple of extra facts about the
comparison function, in addition to its transitivity: its negation must also be
a transitive relation, and it must be strict, i.e.,
@('(not (compare< x x))').</li>

<li>@(':extra-args') may be a list of variables that are used as extra
parameters to all the functions involved.  (If some of your functions don't
require all the arguments, you must wrap them in a lambda in order to accept
the right arguments.)  When using the new syntax with a formals list,
extra-args is not accepted since the formals list already specifies them.</li>

<li>@(':extra-args-guard') may be a term giving a guard that will be required
of the extra-args.</li>

</ul>

<h5>Troubleshooting</h5>

<p>Defsort allows you to specify a lambda rather than a function for most
arguments, and doesn't require that (e.g.) the @(':extra-args-guard') be just a
function call.  But things may break if you use, e.g., a lambda containing an
IF (or AND or OR) as, say, the comparablep predicate.  It is best for
everything to be a simple function call.</p>

<p>There may also be some bad cases when the setting of @(':comparablep') is a
built-in function that ACL2 treats specially or that is in @('minimal-theory').
For example, @(':comparablep atom') used to cause defsort to fail, though now
it has a special hack for that particular case.</p>
")
*defsort-keywords*constant
(defconst *defsort-keywords*
  '(:comparablep :compare< :prefix :comparable-listp :true-listp :weak :extra-args :extra-args-guard :extra-args-stobjs :extra-args-stobj-recognizers))
defsort-functional-inst-substfunction
(defun defsort-functional-inst-subst
  (func-subst wrld)
  (b* (((when (atom func-subst)) nil) (pair (car func-subst))
      (sub (cadr pair))
      (sym (or (and (symbolp sub) sub)
          (and (consp sub)
            (eq (car sub) 'lambda)
            (consp (caddr sub))
            (symbolp (car (caddr sub)))
            (car (caddr sub)))))
      (real-sym (or (cdr (assoc sym (macro-aliases wrld))) sym))
      ((when (and real-sym
           (eq (fgetprop real-sym 'formals :none wrld) :none))) (defsort-functional-inst-subst (cdr func-subst) wrld)))
    (cons pair
      (defsort-functional-inst-subst (cdr func-subst) wrld))))
defsort-functional-inst-fnfunction
(defun defsort-functional-inst-fn
  (thmname func-subst rest-hints state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((mv var-subst rest-hints) (if (eq (car rest-hints) :var-subst)
         (mv (cadr rest-hints) (cddr rest-hints))
         (mv nil rest-hints))))
    `(:use ((:instance (:functional-instance ,THMNAME . ,(DEFSORT-FUNCTIONAL-INST-SUBST FUNC-SUBST (W STATE))) . ,VAR-SUBST)) . ,REST-HINTS)))
defsort-functional-instmacro
(defmacro defsort-functional-inst
  (thmname func-subst &rest rest-hints)
  `(defsort-functional-inst-fn ',THMNAME
    ',FUNC-SUBST
    ',REST-HINTS
    state))
*defsort-empty-ens*constant
(defconst *defsort-empty-ens*
  (make enabled-structure
    :index-of-last-enabling 0
    :theory-array (compress1 'ens0
      (list (list :header :dimensions (list 1)
          :maximum-length 2
          :default nil
          :name 'ens0
          :order nil)))
    :array-name 'ens0
    :array-length 1
    :array-name-root 'ens
    :array-name-suffix 0))
fix-comparablepfunction
(defun fix-comparablep
  (comparablep)
  (cond ((eq comparablep 'atom) '(lambda (x) (not (consp x))))
    (t comparablep)))
defsort-guard-for-termfunction
(defun defsort-guard-for-term
  (term state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((wrld (w state)) ((mv clauses &) (guard-obligation-clauses (cons :term term)
          nil
          *defsort-empty-ens*
          wrld
          state)))
    (mv (untranslate* (conjoin-clauses clauses) nil wrld) state)))
defsort-len-of-cdr-strongtheorem
(defthmd defsort-len-of-cdr-strong
  (implies (consp x) (< (len (cdr x)) (len x)))
  :hints (("goal" :expand ((len x))))
  :rule-classes :linear)
defsort-len-of-cdr-weaktheorem
(defthmd defsort-len-of-cdr-weak
  (<= (len (cdr x)) (len x))
  :hints (("goal" :expand ((len x))))
  :rule-classes :linear)
defsort-nfix-when-not-zptheorem
(defthmd defsort-nfix-when-not-zp
  (implies (not (zp x)) (equal (nfix x) x))
  :hints (("goal" :expand ((nfix x) (zp x)))))
defsort-o-p-when-natptheorem
(defthmd defsort-o-p-when-natp (implies (natp x) (o-p x)))
defsort-o<-of-naturalstheorem
(defthmd defsort-o<-of-naturals
  (implies (and (natp x) (natp y)) (equal (o< x y) (< x y))))
defsort-len-when-not-consptheorem
(defthmd defsort-len-when-not-consp
  (implies (not (consp x)) (equal (len x) 0)))
other
(deftheory defsort-theory
  '(fast-mergesort-admission-1 fast-mergesort-admission-2
    comparable-mergesort-admission-nthcdr
    comparable-mergesort-admission-take
    defsort-len-of-cdr-strong
    defsort-len-of-cdr-weak
    defsort-nfix-when-not-zp
    defsort-o-p-when-natp
    defsort-o<-of-naturals
    defsort-len-when-not-consp
    (:t len)
    (:t nfix)
    natp-compound-recognizer
    zp-compound-recognizer
    rest-n
    (eqlablep)))
defsort-fnfunction
(defun defsort-fn
  (args state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((new-syntaxp (not (keywordp (car args)))) ((mv sort args) (if new-syntaxp
          (mv (car args) (cdr args))
          (mv nil args)))
      (formalsp (and new-syntaxp (consp (car args))))
      ((mv formals args) (if formalsp
          (mv (car args) (cdr args))
          (mv nil args)))
      ((when (and formalsp
           (not (and (symbol-listp formals)
               (consp formals)
               (equal (symbol-name (car formals)) "X"))))) (er soft
          'defsort-fn
          "Defsort: The formals, if provided, must be a symbol-list whose ~
             first element is named X (standing for the list to be sorted)."))
      ((mv kwd-alist args) (extract-keywords 'defsort *defsort-keywords* args nil))
      ((when args) (er soft 'defsort-fn "Defsort: extra arguments"))
      (prefix (getarg :prefix sort kwd-alist))
      ((unless (and prefix (symbolp prefix) (not (keywordp prefix)))) (er soft
          'defsort
          "Defsort requires either a sort name (non-keyword symbol as the ~
               first argument) or a :prefix argument, also a non-keyword ~
               symbol."))
      ((fun (mksym prefix x)) (intern-in-package-of-symbol (concatenate 'string (symbol-name prefix) x)
          (if (equal (symbol-package-name prefix) "COMMON-LISP")
            'foo
            prefix)))
      (sort (or sort (mksym prefix "-SORT")))
      (comparable-listp (getarg :comparable-listp nil kwd-alist))
      (compare< (getarg :compare< nil kwd-alist))
      (comparablep (getarg :comparablep nil kwd-alist))
      (true-listp (getarg :true-listp nil kwd-alist))
      (weak (getarg :weak (not new-syntaxp) kwd-alist))
      ((when (and formalsp (assoc :extra-args kwd-alist))) (er soft
          'defsort
          "Don't use both formals and an :extra-args keyword."))
      (extra-args (if formalsp
          (cdr formals)
          (getarg :extra-args nil kwd-alist)))
      (extra-args-guard (getarg :extra-args-guard t kwd-alist))
      (extra-args-stobjs (getarg :extra-args-stobjs nil kwd-alist))
      (extra-args-stobj-recognizers (getarg :extra-args-stobj-recognizers t kwd-alist))
      ((unless (and (symbol-listp extra-args)
           (not (intersectp-eq '(x y z) extra-args)))) (er soft
          'defsort
          ":extra-args must be a symbol list not containing ~x0, ~x1, or ~x2.~%"
          'x
          'y
          'z))
      ((unless compare<) (er soft
          'defsort
          "Defsort requires :compare< to be specified"))
      (definedp (or comparable-listp (and (not comparablep) true-listp)))
      (comparable-listp (or comparable-listp
          (if comparablep
            (mksym prefix "-LIST-P")
            (and true-listp 'true-listp))))
      (orderedp (mksym prefix "-ORDERED-P"))
      (merge (mksym prefix "-MERGE"))
      (merge-tr (mksym prefix "-MERGE-TR"))
      (fixnum (mksym prefix "-MERGESORT-FIXNUM"))
      (integer (mksym prefix "-MERGESORT-INTEGERS"))
      (comparablep (fix-comparablep comparablep))
      (comparable-inst (if comparablep
          `(lambda (x) (,COMPARABLEP x . ,EXTRA-ARGS))
          `(lambda (x) t)))
      (comparable-listp-inst (if (or comparablep true-listp)
          `(lambda (x) (,COMPARABLE-LISTP x . ,EXTRA-ARGS))
          `(lambda (x) t)))
      (element-list-final-cdr-inst (if true-listp
          `(lambda (x) (not x))
          `(lambda (x) t)))
      ((mv compare-guard state) (defsort-guard-for-term `(,COMPARE< x x . ,EXTRA-ARGS)
          state))
      ((mv comparablep-guard state) (if comparablep
          (defsort-guard-for-term `(,COMPARABLEP x . ,EXTRA-ARGS)
            state)
          (mv t state)))
      (subst1 `((compare< (lambda (x y) (,COMPARE< x y . ,EXTRA-ARGS))) (comparablep ,COMPARABLE-INST)
          (comparable-listp ,COMPARABLE-LISTP-INST)
          (element-list-final-cdr-p ,ELEMENT-LIST-FINAL-CDR-INST)
          (comparable-merge (lambda (x y) (,MERGE x y . ,EXTRA-ARGS)))
          (comparable-orderedp (lambda (x) (,ORDEREDP x . ,EXTRA-ARGS)))
          (comparable-merge-tr (lambda (x y acc) (,MERGE-TR x y ,@EXTRA-ARGS acc)))
          (fast-comparable-mergesort-fixnums (lambda (x len) (,FIXNUM x ,@EXTRA-ARGS len)))
          (fast-comparable-mergesort-integers (lambda (x len) (,INTEGER x ,@EXTRA-ARGS len)))
          (comparable-mergesort (lambda (x) (,SORT x . ,EXTRA-ARGS)))))
      (events1 `(encapsulate nil
          (set-ignore-ok t)
          (local (defthm ,(MKSYM PREFIX "-TYPE-OF-COMPARE<")
              (or (equal (,COMPARE< x y . ,EXTRA-ARGS) t)
                (equal (,COMPARE< x y . ,EXTRA-ARGS) nil))
              :rule-classes :type-prescription))
          ,@(AND COMPARABLEP
       `((LOCAL
          (DEFTHM ,(MKSYM PREFIX "-TYPE-OF-COMPARABLEP")
                  (OR (EQUAL (,COMPARABLEP X . ,EXTRA-ARGS) T)
                      (EQUAL (,COMPARABLEP X . ,EXTRA-ARGS) NIL))
                  :RULE-CLASSES :TYPE-PRESCRIPTION))))
          (local (defthm ,(MKSYM PREFIX "-COMPARE<-TRANSITIVE")
              (implies (and (,COMPARE< x y . ,EXTRA-ARGS)
                  (,COMPARE< y z . ,EXTRA-ARGS))
                (,COMPARE< x z . ,EXTRA-ARGS))))
          ,@(AND (NOT WEAK)
       `((LOCAL
          (DEFTHM ,(MKSYM PREFIX "-COMPARE<-NEGATION-TRANSITIVE")
                  (IMPLIES
                   (AND (NOT (,COMPARE< X Y . ,EXTRA-ARGS))
                        (NOT (,COMPARE< Y Z . ,EXTRA-ARGS)))
                   (NOT (,COMPARE< X Z . ,EXTRA-ARGS)))))
         (LOCAL
          (DEFTHM ,(MKSYM PREFIX "-COMPARE<-STRICT")
                  (NOT (,COMPARE< X X . ,EXTRA-ARGS))))))
          ,@(AND COMPARABLEP (NOT (EQ COMPARE-GUARD T))
       (NOT (EQUAL COMPARE-GUARD `(,COMPARABLEP X)))
       `((LOCAL
          (MAKE-EVENT
           '(:OR
             (DEFTHM DEFSORT-COMPARABLEP-SUFFICIENT
                     (IMPLIES
                      (AND (,COMPARABLEP X . ,EXTRA-ARGS) ,EXTRA-ARGS-GUARD
                           ,EXTRA-ARGS-STOBJ-RECOGNIZERS)
                      ,COMPARE-GUARD)
                     :RULE-CLASSES (:REWRITE :FORWARD-CHAINING))
             (VALUE-TRIPLE
              (ER HARD 'DEFSORT "Couldn't prove that given setting of ~
                              :comparablep, ~x0, implies the guard of the ~
                              comparison function ~x1, which is:~%~x2"
                  ',COMPARABLEP ',COMPARE< ',COMPARE-GUARD)))))))
          ,@(AND COMPARABLEP (NOT (EQ COMPARABLEP-GUARD T))
       (NOT (EQUAL EXTRA-ARGS-GUARD COMPARABLEP-GUARD))
       `((LOCAL
          (MAKE-EVENT
           '(:OR
             (DEFTHM DEFSORT-EXTRA-ARGS-GUARD-SUFFICIENT
                     (IMPLIES
                      (AND ,EXTRA-ARGS-GUARD ,EXTRA-ARGS-STOBJ-RECOGNIZERS)
                      ,COMPARABLEP-GUARD)
                     :RULE-CLASSES (:REWRITE :FORWARD-CHAINING))
             (VALUE-TRIPLE
              (ER HARD 'DEFSORT
                  "Couldn't prove that the guard for the extra-args, ~x0,
                              implies the guard of comparablep (~x1), which is:~%~x2"
                  ',EXTRA-ARGS-GUARD ',COMPARABLEP ',COMPARABLEP-GUARD)))))))
          (local (in-theory (theory 'minimal-theory)))
          (local (in-theory (enable ,(MKSYM PREFIX "-TYPE-OF-COMPARE<")
                ,(MKSYM PREFIX "-COMPARE<-TRANSITIVE")
                defsort-theory)))
          ,@(AND COMPARABLEP (NOT (EQ COMPARE-GUARD T))
       (NOT (EQUAL COMPARE-GUARD `(,COMPARABLEP X)))
       `((LOCAL (IN-THEORY (ENABLE DEFSORT-COMPARABLEP-SUFFICIENT)))))
          ,@(AND COMPARABLEP (NOT (EQ COMPARABLEP-GUARD T))
       (NOT (EQUAL EXTRA-ARGS-GUARD COMPARABLEP-GUARD))
       `((LOCAL (IN-THEORY (ENABLE DEFSORT-EXTRA-ARGS-GUARD-SUFFICIENT)))))
          ,@(AND COMPARABLEP
       `((LOCAL (IN-THEORY (ENABLE ,(MKSYM PREFIX "-TYPE-OF-COMPARABLEP"))))))
          ,@(AND (NOT WEAK)
       `((LOCAL
          (IN-THEORY
           (ENABLE ,(MKSYM PREFIX "-COMPARE<-NEGATION-TRANSITIVE")
                   ,(MKSYM PREFIX "-COMPARE<-STRICT"))))))
          ,@(AND DEFINEDP (OR COMPARABLEP TRUE-LISTP)
       `((LOCAL
          (MAKE-EVENT
           '(:OR
             (DEFTHM DEFSORT-COMPARABLE-LIST-CHECK T :HINTS
                     ((DEFSORT-FUNCTIONAL-INST COMPARABLE-LISTP ,SUBST1
                       :IN-THEORY (ENABLE ,COMPARABLE-LISTP)))
                     :RULE-CLASSES NIL)
             (VALUE-TRIPLE
              (ER HARD 'DEFSORT "The provided value of comparable-listp, ~x0, ~
                           failed consistency checks: either it is not ~
                           defined, or the :true-listp setting was incorrect, ~
                           or the definition doesn't match what we expected."
                  ',COMPARABLE-LISTP)))))))
          ,@(AND (OR COMPARABLEP TRUE-LISTP) (NOT DEFINEDP)
       `((DEFUND ,COMPARABLE-LISTP (X . ,EXTRA-ARGS)
                 (DECLARE
                  (XARGS :GUARD ,EXTRA-ARGS-GUARD :STOBJS ,EXTRA-ARGS-STOBJS))
                 (IF (CONSP X)
                     (AND (,COMPARABLEP (CAR X) . ,EXTRA-ARGS)
                          (,COMPARABLE-LISTP (CDR X) . ,EXTRA-ARGS))
                     ,(IF TRUE-LISTP
                          `(EQ X NIL)
                          T)))))
          ,@(AND COMPARABLEP
       `((LOCAL
          (DEFTHM DEFSORT-COMPARABLEP-OF-CAR
                  (IMPLIES (AND (,COMPARABLE-LISTP X . ,EXTRA-ARGS) (CONSP X))
                           (,COMPARABLEP (CAR X) . ,EXTRA-ARGS))
                  :HINTS
                  (("Goal" :IN-THEORY NIL :EXPAND
                    ((,COMPARABLE-LISTP X . ,EXTRA-ARGS))))))))
          ,@(AND (OR COMPARABLEP TRUE-LISTP)
       `((LOCAL
          (DEFTHM DEFSORT-COMPARABLE-LISTP-OF-CDR
                  (IMPLIES (,COMPARABLE-LISTP X . ,EXTRA-ARGS)
                           (,COMPARABLE-LISTP (CDR X) . ,EXTRA-ARGS))
                  :HINTS
                  (("Goal" :IN-THEORY '(DEFAULT-CDR) :EXPAND
                    ((,COMPARABLE-LISTP X . ,EXTRA-ARGS)
                     (,COMPARABLE-LISTP NIL . ,EXTRA-ARGS))))))
         ,@(AND (CONSP COMPARABLEP)
                `((LOCAL
                   (DEFTHM DEFSORT-COMPARABLEP-OF-CADR
                           (IMPLIES
                            (AND (,COMPARABLE-LISTP X . ,EXTRA-ARGS) (CONSP X)
                                 (CONSP (CDR X)))
                            (,COMPARABLEP (CADR X) . ,EXTRA-ARGS))
                           :HINTS
                           (("Goal" :IN-THEORY NIL :EXPAND
                             ((,COMPARABLE-LISTP X . ,EXTRA-ARGS)
                              (,COMPARABLE-LISTP (CDR X) . ,EXTRA-ARGS))))))))))
          (defund ,ORDEREDP
            (x . ,EXTRA-ARGS)
            (declare (xargs :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD (,COMPARABLE-LISTP X . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)
                :stobjs ,EXTRA-ARGS-STOBJS
                :measure (len x)))
            (cond ((atom x) t)
              ((atom (cdr x)) t)
              ((,COMPARE< (first x) (second x) . ,EXTRA-ARGS) (,ORDEREDP (cdr x) . ,EXTRA-ARGS))
              (t (and (not (,COMPARE< (second x) (first x) . ,EXTRA-ARGS))
                  (,ORDEREDP (cdr x) . ,EXTRA-ARGS)))))
          (defund ,MERGE
            (x y . ,EXTRA-ARGS)
            (declare (xargs :measure (+ (len x) (len y))
                :stobjs ,EXTRA-ARGS-STOBJS
                :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD (,COMPARABLE-LISTP X . ,EXTRA-ARGS)
           (,COMPARABLE-LISTP Y . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)))
            (cond ((atom x) y)
              ((atom y) x)
              ((,COMPARE< (car y) (car x) . ,EXTRA-ARGS) (cons (car y) (,MERGE x (cdr y) . ,EXTRA-ARGS)))
              (t (cons (car x) (,MERGE (cdr x) y . ,EXTRA-ARGS)))))
          (defund ,MERGE-TR
            (x y ,@EXTRA-ARGS acc)
            (declare (xargs :measure (+ (len x) (len y))
                :stobjs ,EXTRA-ARGS-STOBJS
                :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD (,COMPARABLE-LISTP X . ,EXTRA-ARGS)
           (,COMPARABLE-LISTP Y . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)))
            (cond ((atom x) (revappend-without-guard acc y))
              ((atom y) (revappend-without-guard acc x))
              ((,COMPARE< (car y) (car x) . ,EXTRA-ARGS) (,MERGE-TR x (cdr y) ,@EXTRA-ARGS (cons (car y) acc)))
              (t (,MERGE-TR (cdr x) y ,@EXTRA-ARGS (cons (car x) acc)))))
          (defund ,FIXNUM
            (x ,@EXTRA-ARGS len)
            (declare (xargs :measure (nfix len)
                :stobjs ,EXTRA-ARGS-STOBJS
                :guard (and ,EXTRA-ARGS-GUARD
                  ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(,COMPARABLE-LISTP X . ,EXTRA-ARGS)
     T)
                  (natp len)
                  (<= len (len x)))
                :verify-guards nil)
              (type (signed-byte 30) len))
            (cond ((mbe :logic (zp len)
                 :exec (eql (the (signed-byte 30) len) 0)) nil)
              ((eql (the (signed-byte 30) len) 1) (list (car x)))
              (t (let* ((len1 (the (signed-byte 30) (ash (the (signed-byte 30) len) -1))) (len2 (the (signed-byte 30)
                        (- (the (signed-byte 30) len) (the (signed-byte 30) len1))))
                    (part1 (,FIXNUM x ,@EXTRA-ARGS len1))
                    (part2 (,FIXNUM (rest-n len1 x) ,@EXTRA-ARGS len2)))
                  (,MERGE-TR part1 part2 ,@EXTRA-ARGS nil)))))
          (defund ,INTEGER
            (x ,@EXTRA-ARGS len)
            (declare (xargs :measure (nfix len)
                :stobjs ,EXTRA-ARGS-STOBJS
                :guard (and ,EXTRA-ARGS-GUARD
                  ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(,COMPARABLE-LISTP X . ,EXTRA-ARGS)
     T)
                  (natp len)
                  (<= len (len x)))
                :verify-guards nil)
              (type integer len))
            (cond ((mbe :logic (zp len) :exec (eql (the integer len) 0)) nil)
              ((eql (the integer len) 1) (list (car x)))
              (t (let* ((len1 (the integer (ash (the integer len) -1))) (len2 (the integer (- (the integer len) (the integer len1))))
                    (part1 (if (< (the integer len1) (mergesort-fixnum-threshold))
                        (,FIXNUM x ,@EXTRA-ARGS len1)
                        (,INTEGER x ,@EXTRA-ARGS len1)))
                    (part2 (if (< (the integer len2) (mergesort-fixnum-threshold))
                        (,FIXNUM (rest-n len1 x) ,@EXTRA-ARGS len2)
                        (,INTEGER (rest-n len1 x) ,@EXTRA-ARGS len2))))
                  (,MERGE-TR part1 part2 ,@EXTRA-ARGS nil)))))
          (defund ,SORT
            (x . ,EXTRA-ARGS)
            (declare (xargs :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD (,COMPARABLE-LISTP X . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)
                :measure (len x)
                :stobjs ,EXTRA-ARGS-STOBJS
                :verify-guards nil))
            (mbe :logic (cond ((atom x) nil)
                ((atom (cdr x)) (list (car x)))
                (t (let ((half (floor (len x) 2)))
                    (,MERGE (,SORT (take half x) . ,EXTRA-ARGS)
                      (,SORT (nthcdr half x) . ,EXTRA-ARGS) . ,EXTRA-ARGS))))
              :exec (let ((len (len x)))
                (if (< len (mergesort-fixnum-threshold))
                  (,FIXNUM x ,@EXTRA-ARGS len)
                  (,INTEGER x ,@EXTRA-ARGS len)))))
          (local (defthm defsort-subst1-ok
              t
              :rule-classes nil
              :hints ((defsort-functional-inst (:theorem (and (equal (comparable-mergesort x) (comparable-mergesort x))
                     (equal (comparable-orderedp x) (comparable-orderedp x))
                     (equal (comparable-listp x) (comparable-listp x))))
                 ,SUBST1
                 :expand ((,SORT x . ,EXTRA-ARGS) (,MERGE x y . ,EXTRA-ARGS)
                   (,INTEGER x ,@EXTRA-ARGS len)
                   (,FIXNUM x ,@EXTRA-ARGS len)
                   (,MERGE-TR x y ,@EXTRA-ARGS acc)
                   (,ORDEREDP x . ,EXTRA-ARGS)
                   ,@(AND (OR COMPARABLEP TRUE-LISTP) `((,COMPARABLE-LISTP X . ,EXTRA-ARGS))))))))
          (verify-guards ,FIXNUM
            :hints ((defsort-functional-inst fast-comparable-mergesort-fixnums-guards
               ,SUBST1)))
          (verify-guards ,INTEGER
            :hints ((defsort-functional-inst fast-comparable-mergesort-integers-guards
               ,SUBST1)))
          (verify-guards ,SORT
            :hints ((defsort-functional-inst comparable-mergesort-guard ,SUBST1)))
          (defthm ,(MKSYM PREFIX "-SORT-PRESERVES-DUPLICITY")
            (equal (duplicity a (,SORT x . ,EXTRA-ARGS))
              (duplicity a x))
            :hints ((defsort-functional-inst duplicity-of-comparable-mergesort
               ,SUBST1)))
          ,@(AND (OR COMPARABLEP TRUE-LISTP)
       `((DEFTHM ,(MKSYM PREFIX "-SORT-CREATES-COMPARABLE-LISTP")
                 (IMPLIES (,COMPARABLE-LISTP X . ,EXTRA-ARGS)
                          (,COMPARABLE-LISTP (,SORT X . ,EXTRA-ARGS)
                           . ,EXTRA-ARGS))
                 :HINTS
                 ((DEFSORT-FUNCTIONAL-INST
                   COMPARABLE-LISTP-OF-COMPARABLE-MERGESORT ,SUBST1)))))
          (defthm ,(MKSYM PREFIX "-SORT-SORTS")
            (,ORDEREDP (,SORT x . ,EXTRA-ARGS) . ,EXTRA-ARGS)
            :hints ((defsort-functional-inst comparable-orderedp-of-comparable-mergesort
               ,SUBST1
               :in-theory (enable ,ORDEREDP))))
          (defthm ,(MKSYM PREFIX "-SORT-NO-DUPLICATESP-EQUAL")
            (equal (no-duplicatesp-equal (,SORT x . ,EXTRA-ARGS))
              (no-duplicatesp-equal x))
            :hints ((defsort-functional-inst no-duplicatesp-equal-of-comparable-mergesort
               ,SUBST1)))
          (defthm ,(MKSYM PREFIX "-SORT-TRUE-LISTP")
            (true-listp (,SORT x . ,EXTRA-ARGS))
            :rule-classes :type-prescription :hints ((defsort-functional-inst true-listp-of-comparable-mergesort
               ,SUBST1)))
          (defthm ,(MKSYM PREFIX "-SORT-LEN")
            (equal (len (,SORT x . ,EXTRA-ARGS)) (len x))
            :hints ((defsort-functional-inst len-of-comparable-mergesort
               ,SUBST1)))
          (defthm ,(MKSYM PREFIX "-SORT-CONSP")
            (equal (consp (,SORT x . ,EXTRA-ARGS)) (consp x))
            :hints ((defsort-functional-inst consp-of-comparable-mergesort
               ,SUBST1)))
          (defthm ,(MKSYM PREFIX "-SORT-IS-IDENTITY-UNDER-SET-EQUIV")
            (set-equiv (,SORT x . ,EXTRA-ARGS) x)
            :hints ((defsort-functional-inst comparable-mergesort-is-identity-under-set-equiv
               ,SUBST1)))))
      ((when weak) (value events1))
      (insert (mksym prefix "-INSERT"))
      (insertsort (mksym prefix "-INSERTSORT"))
      (subst2 `((compare<-negation-transitive (lambda nil t)) (compare<-strict (lambda nil t))
          (comparable-insert (lambda (elt x) (,INSERT elt x . ,EXTRA-ARGS)))
          (comparable-insertsort (lambda (x) (,INSERTSORT x . ,EXTRA-ARGS))) . ,SUBST1))
      (events2 `((defund ,INSERT
           (elt x . ,EXTRA-ARGS)
           (declare (xargs :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD
           ,@(AND COMPARABLEP `((,COMPARABLEP ELT . ,EXTRA-ARGS)))
           (,COMPARABLE-LISTP X . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)
               :stobjs ,EXTRA-ARGS-STOBJS
               :measure (len x)))
           (if (atom x)
             (list elt)
             (if (,COMPARE< (car x) elt . ,EXTRA-ARGS)
               (cons (car x) (,INSERT elt (cdr x) . ,EXTRA-ARGS))
               (cons elt x)))) (defund ,INSERTSORT
            (x . ,EXTRA-ARGS)
            (declare (xargs :guard ,(IF (OR COMPARABLEP TRUE-LISTP)
     `(AND ,EXTRA-ARGS-GUARD (,COMPARABLE-LISTP X . ,EXTRA-ARGS))
     EXTRA-ARGS-GUARD)
                :stobjs ,EXTRA-ARGS-STOBJS
                :verify-guards nil
                :measure (len x)))
            (if (atom x)
              nil
              (,INSERT (car x)
                (,INSERTSORT (cdr x) . ,EXTRA-ARGS) . ,EXTRA-ARGS)))
          (local (defthm defsort-subst2-ok
              t
              :rule-classes nil
              :hints ((defsort-functional-inst (:theorem (equal (comparable-insertsort x) (comparable-insertsort x)))
                 ,SUBST2
                 :expand ((,INSERT elt x . ,EXTRA-ARGS) (,INSERTSORT x . ,EXTRA-ARGS))))))
          (verify-guards ,INSERTSORT
            :hints ((defsort-functional-inst comparable-insertsort-guard
               ,SUBST2)))
          (defthm ,(MKSYM PREFIX "-MERGESORT-EQUALS-INSERTSORT")
            (equal (,SORT x . ,EXTRA-ARGS)
              (,INSERTSORT x . ,EXTRA-ARGS))
            :hints ((defsort-functional-inst comparable-mergesort-equals-comparable-insertsort
               ,SUBST2)))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-PRESERVES-DUPLICITY")
            (equal (duplicity a (,INSERTSORT x . ,EXTRA-ARGS))
              (duplicity a x))
            :hints (("goal" :use ,(MKSYM PREFIX "-SORT-PRESERVES-DUPLICITY")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-PRESERVES-DUPLICITY")))))
          ,@(AND (OR COMPARABLEP TRUE-LISTP)
       `((DEFTHM ,(MKSYM PREFIX "-INSERTSORT-CREATES-COMPARABLE-LISTP")
                 (IMPLIES (,COMPARABLE-LISTP X . ,EXTRA-ARGS)
                          (,COMPARABLE-LISTP (,INSERTSORT X . ,EXTRA-ARGS)
                           . ,EXTRA-ARGS))
                 :HINTS
                 (("goal" :USE ,(MKSYM PREFIX "-SORT-CREATES-COMPARABLE-LISTP")
                   :IN-THEORY
                   (DISABLE
                    ,(MKSYM PREFIX "-SORT-CREATES-COMPARABLE-LISTP")))))))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-SORTS")
            (,ORDEREDP (,INSERTSORT x . ,EXTRA-ARGS) . ,EXTRA-ARGS)
            :hints (("goal" :use ,(MKSYM PREFIX "-SORT-SORTS")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-SORTS")))))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-NO-DUPLICATESP-EQUAL")
            (equal (no-duplicatesp-equal (,INSERTSORT x . ,EXTRA-ARGS))
              (no-duplicatesp-equal x))
            :hints (("goal" :use ,(MKSYM PREFIX "-SORT-NO-DUPLICATESP-EQUAL")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-NO-DUPLICATESP-EQUAL")))))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-TRUE-LISTP")
            (true-listp (,INSERTSORT x . ,EXTRA-ARGS))
            :rule-classes :type-prescription :hints (("goal" :use ,(MKSYM PREFIX "-SORT-TRUE-LISTP")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-TRUE-LISTP")))))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-LEN")
            (equal (len (,INSERTSORT x . ,EXTRA-ARGS)) (len x))
            :hints (("goal" :use ,(MKSYM PREFIX "-SORT-LEN")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-LEN")))))
          (defthm ,(MKSYM PREFIX "-INSERTSORT-CONSP")
            (equal (consp (,INSERTSORT x . ,EXTRA-ARGS)) (consp x))
            :hints (("goal" :use ,(MKSYM PREFIX "-SORT-CONSP")
               :in-theory (disable ,(MKSYM PREFIX "-SORT-CONSP"))))))))
    (value (append events1 events2))))
defsortmacro
(defmacro defsort
  (&rest args)
  `(make-event (defsort-fn ',ARGS state)))