apply

(in-package "ACL2")

(when-pass-2 (defun badge
    (fn)
    (declare (xargs :guard t :mode :program))
    (cond ((apply$-primp fn) (badge-prim fn))
      ((eq fn 'badge) *generic-tame-badge-1*)
      ((eq fn 'tamep) *generic-tame-badge-1*)
      ((eq fn 'tamep-functionp) *generic-tame-badge-1*)
      ((eq fn 'suitably-tamep-listp) *generic-tame-badge-3*)
      ((eq fn 'apply$) *apply$-badge*)
      ((eq fn 'ev$) *ev$-badge*)
      (t (badge-userfn fn))))
  (in-theory (disable apply$-primp badge-prim))
  (defabbrev tamep-lambdap
    (fn)
    (and (lambda-object-shapep fn)
      (symbol-listp (lambda-object-formals fn))
      (tamep (lambda-object-body fn))))
  (mutual-recursion (defun tamep
      (x)
      (declare (xargs :measure (acl2-count x) :guard t :mode :program))
      (cond ((atom x) (symbolp x))
        ((eq (car x) 'quote) (and (consp (cdr x)) (null (cddr x))))
        ((symbolp (car x)) (let ((bdg (badge (car x))))
            (cond ((null bdg) nil)
              ((eq (access apply$-badge bdg :ilks) t) (suitably-tamep-listp (access apply$-badge bdg :arity)
                  nil
                  (cdr x)))
              (t (suitably-tamep-listp (access apply$-badge bdg :arity)
                  (access apply$-badge bdg :ilks)
                  (cdr x))))))
        ((consp (car x)) (let ((fn (car x)))
            (and (tamep-lambdap fn)
              (suitably-tamep-listp (length (cadr fn)) nil (cdr x)))))
        (t nil)))
    (defun tamep-functionp
      (fn)
      (declare (xargs :measure (acl2-count fn) :guard t))
      (if (symbolp fn)
        (let ((bdg (badge fn)))
          (and bdg (eq (access apply$-badge bdg :ilks) t)))
        (and (consp fn) (tamep-lambdap fn))))
    (defun suitably-tamep-listp
      (n flags args)
      (declare (xargs :measure (acl2-count args)
          :guard (and (natp n) (true-listp flags))))
      (cond ((zp n) (null args))
        ((atom args) nil)
        (t (and (let ((arg (car args)))
              (case (car flags)
                (:fn (and (consp arg)
                    (eq (car arg) 'quote)
                    (consp (cdr arg))
                    (null (cddr arg))
                    (tamep-functionp (cadr arg))))
                (:expr (and (consp arg)
                    (eq (car arg) 'quote)
                    (consp (cdr arg))
                    (null (cddr arg))
                    (tamep (cadr arg))))
                (otherwise (tamep arg))))
            (suitably-tamep-listp (- n 1) (cdr flags) (cdr args)))))))
  (mutual-recursion (defun apply$
      (fn args)
      (declare (xargs :guard (apply$-guard fn args)
          :guard-hints (("Goal" :do-not-induct t))
          :mode :program))
      (cond ((consp fn) (apply$-lambda fn args))
        ((apply$-primp fn) (apply$-prim fn args))
        ((eq fn 'badge) (badge (car args)))
        ((eq fn 'tamep) (tamep (car args)))
        ((eq fn 'tamep-functionp) (tamep-functionp (car args)))
        ((eq fn 'suitably-tamep-listp) (ec-call (suitably-tamep-listp (car args) (cadr args) (caddr args))))
        ((eq fn 'apply$) (if (tamep-functionp (car args))
            (ec-call (apply$ (car args) (cadr args)))
            (untame-apply$ fn args)))
        ((eq fn 'ev$) (if (tamep (car args))
            (ev$ (car args) (cadr args))
            (untame-apply$ fn args)))
        (t (apply$-userfn fn args))))
    (defun apply$-lambda
      (fn args)
      (declare (xargs :guard (apply$-lambda-guard fn args)
          :guard-hints (("Goal" :do-not-induct t))))
      (apply$-lambda-logical fn args))
    (defun ev$
      (x a)
      (declare (xargs :guard t))
      (cond ((not (tamep x)) (untame-ev$ x a))
        ((variablep x) (ec-call (cdr (ec-call (assoc-equal x a)))))
        ((fquotep x) (cadr x))
        ((eq (car x) 'if) (if (ev$ (cadr x) a)
            (ev$ (caddr x) a)
            (ev$ (cadddr x) a)))
        ((eq (car x) 'apply$) (apply$ 'apply$ (list (cadr (cadr x)) (ev$ (caddr x) a))))
        ((eq (car x) 'ev$) (apply$ 'ev$ (list (cadr (cadr x)) (ev$ (caddr x) a))))
        (t (apply$ (car x) (ev$-list (cdr x) a)))))
    (defun ev$-list
      (x a)
      (declare (xargs :guard t))
      (cond ((atom x) nil)
        (t (cons (ev$ (car x) a) (ev$-list (cdr x) a))))))
  (mutual-recursion (defun quick-check-for-tamenessp
      (name term wrld)
      (declare (xargs :mode :program))
      (cond ((variablep term) t)
        ((fquotep term) t)
        (t (let ((fn (ffn-symb term)))
            (cond ((flambdap fn) (and (quick-check-for-tamenessp name (lambda-body fn) wrld)
                  (quick-check-for-tamenessp-listp name (fargs term) wrld)))
              ((eq name fn) (quick-check-for-tamenessp-listp name (fargs term) wrld))
              (t (let ((bdg (executable-badge fn wrld)))
                  (and bdg
                    (eq (access apply$-badge bdg :ilks) t)
                    (quick-check-for-tamenessp-listp name (fargs term) wrld)))))))))
    (defun quick-check-for-tamenessp-listp
      (name terms wrld)
      (declare (xargs :mode :program))
      (cond ((endp terms) t)
        (t (and (quick-check-for-tamenessp name (car terms) wrld)
            (quick-check-for-tamenessp-listp name (cdr terms) wrld))))))
  (defun accumulate-ilk
    (var ilk alist)
    (declare (xargs :mode :program))
    (let ((temp (assoc-eq var alist)))
      (cond ((null temp) (if (eq ilk :unknown)
            (mv nil alist)
            (mv nil (cons (cons var ilk) alist))))
        ((eq ilk :unknown) (mv nil alist))
        ((eq ilk (cdr temp)) (mv nil alist))
        (t (mv (msg "The variable ~x0 is used both as ~#1~[a function (ilk = ~
                  :FN)~/an expression (ilk = :EXPR)~/an ordinary object (ilk ~
                  = NIL)~] and as ~#2~[a function (ilk = :FN)~/an expression ~
                  (ilk = :EXPR)~/an ordinary object (ilk = NIL)~]."
              var
              (cond ((eq (cdr temp) :fn) 0)
                ((eq (cdr temp) :expr) 1)
                (t 2))
              (cond ((eq ilk :fn) 0) ((eq ilk :expr) 1) (t 2)))
            nil)))))
  (defun convert-ilk-alist-to-ilks1
    (formals alist)
    (declare (xargs :mode :program))
    (cond ((endp formals) nil)
      (t (cons (cdr (assoc-eq (car formals) alist))
          (convert-ilk-alist-to-ilks1 (cdr formals) alist)))))
  (defun convert-ilk-alist-to-ilks
    (formals alist)
    (declare (xargs :mode :program))
    (let ((temp (convert-ilk-alist-to-ilks1 formals alist)))
      (if (all-nils temp)
        t
        temp)))
  (defun changed-functional-or-expressional-formalp
    (formals ilks actuals)
    (declare (xargs :mode :program))
    (cond ((endp formals) nil)
      ((and (or (eq (car ilks) :fn) (eq (car ilks) :expr))
         (not (eq (car formals) (car actuals)))) (list (car formals) (car ilks) (car actuals)))
      (t (changed-functional-or-expressional-formalp (cdr formals)
          (cdr ilks)
          (cdr actuals)))))
  (defun weak-well-formed-lambda-objectp
    (x wrld)
    (declare (xargs :mode :program))
    (case-match x
      (('lambda formals body) (and (arglistp formals)
          (termp body wrld)
          (subsetp-eq (all-vars body) formals)))
      (('lambda formals dcl body) (declare (ignore dcl))
        (and (arglistp formals)
          (termp body wrld)
          (subsetp-eq (all-vars body) formals)))
      (& nil)))
  (mutual-recursion (defun guess-ilks-alist
      (fn new-badge term ilk wrld alist)
      (declare (xargs :mode :program))
      (cond ((variablep term) (accumulate-ilk term ilk alist))
        ((fquotep term) (cond ((eq ilk :fn) (cond ((symbolp (cadr term)) (cond ((and (eq fn (cadr term)) (not (executable-badge fn wrld))) (mv (msg "~x0 cannot be badged because a :FN slot in its body is ~
                    occupied by a quoted reference to ~x0 itself; recursion ~
                    through APPLY$ is not permitted except when the function ~
                    was admitted with XARGS :LOOP$-RECURSION T, which only ~
                    permits such recursion in LOOP$s."
                          fn)
                        nil))
                    ((executable-tamep-functionp (cadr term) wrld) (mv nil alist))
                    (t (mv (msg "~x0 cannot be badged because a :FN slot in its ~
                      body is occupied by a quoted symbol, ~x1, that is not a ~
                      tame function."
                          fn
                          term)
                        nil))))
                ((consp (cadr term)) (cond ((weak-well-formed-lambda-objectp (cadr term) wrld) (cond ((and (ffnnamep fn (lambda-object-body (cadr term)))
                           (not (executable-badge fn wrld))) (mv (msg "~x0 cannot be badged because a :FN slot in its ~
                           body is occupied by a lambda object, ~x1, that ~
                           recursively calls ~x0; recursion through APPLY$ is ~
                           not permitted unless the function was admitted ~
                           with XARGS :LOOP$-RECURSION T, which only permits ~
                           such recursion in LOOP$s."
                              fn
                              term)
                            nil))
                        ((executable-tamep-lambdap (cadr term) wrld) (mv nil alist))
                        (t (mv (msg "~x0 cannot be badged because a :FN slot in ~
                             its body is occupied by a lambda object, ~x1, ~
                             whose body is not tame."
                              fn
                              term)
                            nil))))
                    (t (mv (msg "~x0 will not be badged because a :FN slot in ~
                           its body is occupied by a quoted cons object, ~x1, ~
                           that is not a well-formed, fully-translated, ~
                           closed lambda object.  The default behavior of ~
                           APPLY$ on ill-formed input is nonsensical, e.g., ~
                           unquoted numbers are treated like variables and ~
                           macros are treated like undefined functions.  It ~
                           is unwise to exploit this default behavior!"
                          fn
                          term)
                        nil))))
                (t (mv (msg "~x0 cannot be badged because a :FN slot in its ~
                    body is occupied by a quoted constant, ~x1, that does not ~
                    denote a tame function symbol or lambda object."
                      fn
                      term)
                    nil))))
            ((eq ilk :expr) (cond ((termp (cadr term) wrld) (cond ((ffnnamep fn (cadr term)) (mv (msg "~x0 cannot be badged because an :EXPR slot ~
                         in its body is occupied by a quoted term, ~x1, that ~
                         calls ~x0; recursion through EV$ is not permitted!"
                          fn
                          term)
                        nil))
                    ((executable-tamep (cadr term) wrld) (mv nil alist))
                    (t (mv (msg "~x0 cannot be badged because an :EXPR ~
                           slot in its body is occupied by a quoted term, ~
                           ~x1, that is not tame."
                          fn
                          term)
                        nil))))
                (t (mv (msg "~x0 will not be badged because an :EXPR slot in its ~
                    body is occupied by a quoted object, ~x1, that is not a ~
                    well-formed, fully-translated ACL2 term.  The default ~
                    behavior of EV$ on ill-formed input is nonsensical, e.g., ~
                    unquoted numbers are treated like variables and macros ~
                    are treated like undefined functions.  It is unwise to ~
                    exploit this default behavior!"
                      fn
                      term)
                    nil))))
            (t (mv nil alist))))
        ((flambdap (ffn-symb term)) (mv (msg "There are not supposed to be any ACL2 lambda applications in ~
              the term being analyzed by guess-ilks-alist, but we have ~
              encountered ~x0!  This really indicates a coding error in ACL2 ~
              and is not your fault!  Please tell the implementors."
              term)
            nil))
        ((or (eq ilk :fn) (eq ilk :expr)) (mv (msg "~x0 cannot be badged because ~#1~[a :FN~/an :EXPR~] slot in ~
              its body is occupied by a call of ~x2.  All :FN and :EXPR slots ~
              must be occupied by either variable symbols or quoted constants ~
              denoting tame functions."
              fn
              (if (eq ilk :fn)
                0
                1)
              (ffn-symb term))
            nil))
        ((eq fn (ffn-symb term)) (cond (new-badge (mv-let (msg alist1)
                (guess-ilks-alist-list fn
                  new-badge
                  (fargs term)
                  (access apply$-badge new-badge :ilks)
                  wrld
                  alist)
                (cond ((or msg (not (equal alist1 alist))) (mv (msg "The first pass of the badger on ~x0 produced the proposed ~
                    badge ~x1, but when we ran the second pass -- in which ~
                    recursive calls of ~x0 are assumed to have that badge -- ~
                    we ~#2~[got this error message:  ~@3~/the badger posited ~
                    a different alist mapping formals to ilks, namely ~x4.~]"
                        fn
                        new-badge
                        (if msg
                          0
                          1)
                        msg
                        alist1)
                      nil))
                  ((not (eq (access apply$-badge new-badge :ilks) t)) (let ((triple (changed-functional-or-expressional-formalp (formals fn wrld)
                           (access apply$-badge new-badge :ilks)
                           (fargs term))))
                      (cond (triple (mv (msg "The first pass of the badger on ~x0 produced ~
                               the proposed badge ~x1, but during the second ~
                               pass -- in which recursive calls of ~x0 are ~
                               assumed to have that badge -- we found that ~
                               the formal parameter ~x2, which was assigned ~
                               ilk ~x3, was not passed identically into a ~
                               recursive call of ~x0.  Instead, the actual ~
                               ~x4 was passed for the new value of ~x2.  No ~
                               warrant can be issued for ~x0."
                              fn
                              new-badge
                              (car triple)
                              (cadr triple)
                              (caddr triple))
                            nil))
                        (t (mv nil alist)))))
                  (t (mv nil alist)))))
            (t (guess-ilks-alist-list fn
                new-badge
                (fargs term)
                :unknown* wrld
                alist))))
        (t (let ((bdg (executable-badge (ffn-symb term) wrld)))
            (cond ((null bdg) (mv (msg "~x0 calls the function ~x1 which does not have a badge.  ~
                    You may be able to remedy this by executing ~x2 but then ~
                    again it is possible you've done that already and ~x1 ~
                    cannot be badged, in which case neither can ~x0."
                    fn
                    (ffn-symb term)
                    `(defbadge ,(FFN-SYMB TERM)))
                  nil))
              (t (guess-ilks-alist-list fn
                  new-badge
                  (fargs term)
                  (access apply$-badge bdg :ilks)
                  wrld
                  alist)))))))
    (defun guess-ilks-alist-list
      (fn new-badge terms ilks wrld alist)
      (declare (xargs :mode :program))
      (cond ((endp terms) (mv nil alist))
        (t (mv-let (msg alist1)
            (guess-ilks-alist fn
              new-badge
              (car terms)
              (cond ((eq ilks :unknown*) :unknown)
                ((eq ilks t) nil)
                (t (car ilks)))
              wrld
              alist)
            (cond (msg (mv msg nil))
              (t (guess-ilks-alist-list fn
                  new-badge
                  (cdr terms)
                  (cond ((eq ilks :unknown*) :unknown*)
                    ((eq ilks t) t)
                    (t (cdr ilks)))
                  wrld
                  alist1))))))))
  (defun nonsensical-justification-term
    (fn wrld)
    (declare (xargs :mode :program))
    (let ((just (getpropc fn 'justification nil wrld)))
      (if just
        (let ((m (access justification just :measure)) (rel (access justification just :rel))
            (mp (access justification just :mp)))
          (fcons-term* rel m (fcons-term* mp 'x)))
        *t*)))
  (defun bad-ancestor1
    (flg jflg x bad-fns wrld seen)
    (declare (xargs :mode :program))
    (cond ((and seen (symbolp seen)) seen)
      (flg (cond ((null x) seen)
          (t (bad-ancestor1 nil
              jflg
              (car x)
              bad-fns
              wrld
              (bad-ancestor1 t jflg (cdr x) bad-fns wrld seen)))))
      ((variablep x) seen)
      ((fquotep x) seen)
      ((flambda-applicationp x) (bad-ancestor1 nil
          jflg
          (lambda-body (ffn-symb x))
          bad-fns
          wrld
          (bad-ancestor1 t jflg (cdr x) bad-fns wrld seen)))
      ((member-eq (ffn-symb x) bad-fns) (ffn-symb x))
      ((member-eq (ffn-symb x) seen) (bad-ancestor1 t jflg (fargs x) bad-fns wrld seen))
      (jflg (bad-ancestor1 nil
          jflg
          (body (ffn-symb x) nil wrld)
          bad-fns
          wrld
          (bad-ancestor1 t
            jflg
            (fargs x)
            bad-fns
            wrld
            (bad-ancestor1 nil
              jflg
              (nonsensical-justification-term (ffn-symb x) wrld)
              bad-fns
              wrld
              (cons (ffn-symb x) seen)))))
      (t (bad-ancestor1 nil
          jflg
          (body (ffn-symb x) nil wrld)
          bad-fns
          wrld
          (bad-ancestor1 t
            jflg
            (fargs x)
            bad-fns
            wrld
            (cons (ffn-symb x) seen))))))
  (defun bad-ancestor
    (jflg term bad-fns wrld)
    (declare (xargs :mode :program))
    (let ((ans (bad-ancestor1 nil jflg term bad-fns wrld nil)))
      (if (and ans (symbolp ans))
        ans
        nil)))
  (defun not-pre-apply$-definable
    (fnp x wrld)
    (declare (xargs :mode :program))
    (bad-ancestor t
      (if fnp
        (fcons-term x (formals x wrld))
        x)
      *apply$-userfn-callers*
      wrld))
  (defun lex-measure-terms
    (term)
    (declare (xargs :mode :program))
    (cond ((variablep term) nil)
      ((fquotep term) (cond ((equal term *nil*) t) (t nil)))
      ((and (eq (ffn-symb term) 'cons)
         (nvariablep (fargn term 1))
         (not (fquotep (fargn term 1)))
         (eq (ffn-symb (fargn term 1)) 'nfix)) (let ((temp (lex-measure-terms (fargn term 2))))
          (cond ((null temp) nil)
            (t (cons (fargn term 1)
                (if (eq temp t)
                  nil
                  temp))))))
      (t nil)))
  (defun g2-justification
    (fn ens wrld)
    (declare (xargs :mode :program))
    (cond ((not (recursivep fn nil wrld)) (mv t nil))
      (t (let ((just (getpropc fn 'justification nil wrld)))
          (cond ((null just) (mv (er hard
                  'warranted-justification
                  "~x0 is marked with a non-nil RECURSIVEP property but its ~
                   JUSTIFICATION property is nil!"
                  fn)
                nil))
            (t (let* ((m (access justification just :measure)) (rel (access justification just :rel))
                  (mp (access justification just :mp)))
                (cond ((eq rel 'o<) (mv-let (ts ttree)
                      (type-set m nil nil nil ens wrld nil nil nil)
                      (declare (ignore ttree))
                      (cond ((ts-subsetp ts *ts-non-negative-integer*) (cond ((not (eq mp 'o-p)) (mv nil
                                (msg "~x0 cannot be warranted because its ~
                                justification's domain is ~x1 instead of O-P ~
                                as required for its natural-number measure."
                                  fn
                                  mp)))
                            (t (mv t nil))))
                        (t (let ((defthm-event `(defthm ,(PACKN-POS (LIST "NATP-MEASURE-OF-" FN) FN)
                                 (natp ,M)
                                 :rule-classes nil)))
                            (mv t
                              `((make-event (pprogn (observation (cons 'defwarrant ',FN)
                                     "Since ~x0 is justified with O<, defwarrant ~
                                  insists that ~x0's measure, ~x1, satisfy ~
                                  NATP.  Syntactic considerations fail to ~
                                  establish this.  So to warrant ~x0 we must ~
                                  prove~%~%~X23~%~%"
                                     ',FN
                                     ',M
                                     ',DEFTHM-EVENT
                                     nil)
                                   (value '(value-triple :invisible)))) ,DEFTHM-EVENT)))))))
                  ((eq rel 'l<) (cond ((not (eq mp 'lexp)) (mv nil
                          (msg "~x0 cannot be warranted because its ~
                            justification's domain is ~x1 but defwarrant ~
                            requires that when the well-founded relation is ~
                            l< the domain be lexp."
                            fn
                            mp)))
                      (t (mv t nil))))
                  (t (mv nil
                      (msg "~x0 cannot be warranted because it was justified ~
                            with well-founded relation ~x1.  Defwarrant ~
                            requires that the justification use either O< (on ~
                            domain O-P) or L< (on domain LEXP) and that in ~
                            the O< case the measure must return a natural ~
                            number, not a larger ordinal."
                        fn
                        rel)))))))))))
  (defun badger
    (fn wrld)
    (declare (xargs :mode :program))
    (let ((formals (formals fn wrld)) (body (expand-all-lambdas (body fn nil wrld))))
      (mv-let (msg alist0)
        (guess-ilks-alist fn nil body :unknown wrld nil)
        (cond (msg (mv msg nil))
          (t (let* ((new-ilks (convert-ilk-alist-to-ilks formals alist0)) (alist1 (pairlis$ formals
                    (if (eq new-ilks t)
                      nil
                      new-ilks)))
                (new-badge (make apply$-badge
                    :arity (arity fn wrld)
                    :out-arity (length (getpropc fn 'stobjs-out nil wrld))
                    :ilks new-ilks)))
              (mv-let (msg alist2)
                (guess-ilks-alist fn new-badge body nil wrld alist1)
                (cond (msg (mv msg nil))
                  ((equal alist1 alist2) (mv nil new-badge))
                  (t (mv (er hard
                        'badger
                        "The second pass of the badger produced a different alist ~
                     than the first!  The (completed) alist produced by the ~
                     first pass is ~x0 but the alist produced by the second ~
                     pass is ~x1.  This must be some kind of coding error in ~
                     ACL2.  Please report this to the implementors."
                        alist1
                        alist2)
                      nil))))))))))
  (defun recognize-badge-userfn-structure-op1
    (new-lst old-lst)
    (declare (xargs :mode :program))
    (cond ((endp new-lst) (cond ((endp old-lst) (mv (er hard
                'badge-table-guard
                "~@0we found no changed tuple."
                *badge-table-guard-msg*)
              nil))
          (t (mv (er hard
                'badge-table-guard
                "~@0the new value doesn't include all the function symbols in ~
                 the old one.  The first omitted tuple from the old list is ~
                 ~x1."
                *badge-table-guard-msg*
                (car old-lst))
              nil))))
      ((endp old-lst) (mv (er hard
            'badge-table-guard
            "~@0the new value contains a new tuple, ~x1, that is not at the ~
             front of the list."
            *badge-table-guard-msg*
            (car new-lst))
          nil))
      ((equal (car new-lst) (car old-lst)) (recognize-badge-userfn-structure-op1 (cdr new-lst)
          (cdr old-lst)))
      ((weak-badge-userfn-structure-tuplep (car new-lst)) (let* ((new-tuple (car new-lst)) (old-tuple (car old-lst))
            (new-fn (car new-tuple))
            (new-warrantp (access-badge-userfn-structure-tuple-warrantp new-tuple))
            (new-badge (access-badge-userfn-structure-tuple-badge new-tuple))
            (old-fn (car old-tuple))
            (old-warrantp (access-badge-userfn-structure-tuple-warrantp old-tuple))
            (old-badge (access-badge-userfn-structure-tuple-badge old-tuple)))
          (cond ((and (eq old-fn new-fn)
               (eq old-warrantp nil)
               (eq new-warrantp t)
               (equal old-badge new-badge)
               (equal (cdr old-lst) (cdr new-lst))) (mv :changed new-tuple))
            (t (mv (er hard
                  'badge-table-guard
                  "~@0the first changed tuple does not just flip the ~
                   warrantp flag.  The proposed new tuple is ~x1 and the ~
                   corresponding old tuple is ~x2."
                  *badge-table-guard-msg*
                  new-tuple
                  old-tuple)
                nil)))))
      (t (mv (er hard
            'badge-table-guard
            "~@0the first changed element was ill-formed.  The proposed new ~
               element is ~x1 and the corresponding old tuple is ~x2."
            *badge-table-guard-msg*
            (car new-lst)
            (car old-lst))
          nil))))
  (defun recognize-badge-userfn-structure-op
    (new-lst old-lst)
    (declare (xargs :mode :program))
    (cond ((and (consp new-lst) (equal (cdr new-lst) old-lst)) (cond ((weak-badge-userfn-structure-tuplep (car new-lst)) (mv :new (car new-lst)))
          (t (mv (er hard
                'badge-table-guard
                "~@0the proposed new element, ~x1, is ill-formed."
                *badge-table-guard-msg*
                (car new-lst))
              nil))))
      (t (recognize-badge-userfn-structure-op1 new-lst old-lst))))
  (defun get-defun-body
    (fn ctx wrld)
    (declare (xargs :mode :program))
    (let ((body (car (last (get-defun-event fn wrld)))))
      (and body
        (mv-let (erp tbody)
          (translate-cmp body
            t
            nil
            t
            ctx
            wrld
            (default-state-vars nil
              :temp-touchable-vars t
              :temp-touchable-fns t))
          (cond ((null erp) tbody)
            (t (er hard
                ctx
                "An attempt to translate the body of function symbol ~
                         ~x0 failed unexpectedly."
                fn)))))))
  (defun ok-defbadge
    (fn wrld)
    (declare (xargs :mode :program))
    (let ((bdg (and (symbolp fn) (get-badge fn wrld))) (body (and (symbolp fn)
            (or (body fn nil wrld) (get-defun-body fn 'defbadge wrld)))))
      (cond (bdg (mv nil t bdg))
        ((not (and (symbolp fn) (arity fn wrld) body)) (mv (msg "Only defined function symbols can be badged and ~x0 is not one."
              fn)
            nil
            nil))
        ((untouchable-fn-p fn wrld nil) (mv (msg "~x0 has been declared untouchable and so cannot be badged."
              fn)
            nil
            nil))
        ((member-eq fn *blacklisted-apply$-fns*) (mv (msg "~x0 cannot be badged because apply$ is prohibited from ~
                    calling it.  This is generally because its Common Lisp ~
                    behavior is different from its logical behavior."
              fn)
            nil
            nil))
        ((null (bad-ancestor nil body *apply$-userfn-callers* wrld)) (mv nil
            nil
            (make apply$-badge
              :arity (arity fn wrld)
              :out-arity (length (getpropc fn 'stobjs-out nil wrld))
              :ilks t)))
        ((cdr (getpropc fn 'recursivep nil wrld)) (mv (msg "~x0 cannot be badged because it is mutually recursive clique ~
                with ~&1.  Unfortunately, we cannot yet analyze such cliques."
              fn
              (remove1-eq fn (getpropc fn 'recursivep nil wrld)))
            nil
            nil))
        ((quick-check-for-tamenessp fn body wrld) (mv nil
            nil
            (make apply$-badge
              :arity (arity fn wrld)
              :out-arity (length (getpropc fn 'stobjs-out nil wrld))
              :ilks t)))
        (t (mv-let (msg badge)
            (badger fn wrld)
            (cond (msg (mv msg nil nil)) (t (mv nil nil badge))))))))
  (defun chk-acceptable-defwarrant1
    (fn ens wrld)
    (declare (xargs :mode :program))
    (cond ((or (apply$-primp fn)
         (assoc-eq fn *apply$-boot-fns-badge-alist*)) (mv nil t))
      ((eq (getpropc fn 'symbol-class nil wrld) :program) (mv t
          (msg "Defwarrant expects a defined, :logic mode function symbol as ~
                its argument and ~x0 is not one."
            fn)))
      (t (let ((bad-fn (if (eq fn 'do$)
               nil
               (not-pre-apply$-definable nil
                 (nonsensical-justification-term fn wrld)
                 wrld))))
          (cond (bad-fn (mv t
                (msg "~x0 cannot be warranted because some part of its ~
                      justification (i.e., its measure, well-founded ~
                      relation, or domain predicate) ancestrally calls or is ~
                      justified in terms of ~x1."
                  fn
                  bad-fn)))
            (t (let ((body (body fn nil wrld)))
                (cond ((null (bad-ancestor nil body *apply$-userfn-callers* wrld)) (mv nil nil))
                  (t (mv-let (flg val)
                      (g2-justification fn ens wrld)
                      (cond (flg (mv nil val)) (t (mv t val)))))))))))))
  (defun badge-table-guard1
    (new-lst old-lst ens wrld)
    (declare (xargs :mode :program))
    (cond ((null new-lst) t)
      (t (mv-let (op tuple)
          (recognize-badge-userfn-structure-op new-lst old-lst)
          (let ((fn (car tuple)) (warrantp (access-badge-userfn-structure-tuple-warrantp tuple))
              (badge (access-badge-userfn-structure-tuple-badge tuple)))
            (and (or (eq op :new)
                (eq op :changed)
                (er hard
                  'badge-table-guard
                  "Recognize-badge-userfn-structure-op returned op = ~x0 when ~
                  it is supposed be either :NEW or :CHANGED."
                  op))
              (if (eq op :new)
                (and (symbolp fn)
                  (arity fn wrld)
                  (not (assoc-eq fn old-lst))
                  (booleanp warrantp)
                  (mv-let (msg flg correct-badge)
                    (ok-defbadge fn wrld)
                    (declare (ignore flg))
                    (cond (msg (er hard
                          'badge-table-guard
                          "~@0the badge proposed for ~x1 was ~x2, but ~
                                 badger reports: ~@3"
                          *badge-table-guard-msg*
                          fn
                          badge
                          msg))
                      ((not (equal badge correct-badge)) (er hard
                          'badge-table-guard
                          "~@0the badge proposed for ~x1 was ~x2 but the ~
                             actual badge computed by the badger is ~x3"
                          *badge-table-guard-msg*
                          fn
                          badge
                          correct-badge))
                      (t t))))
                t)
              (if (eq warrantp t)
                (and (or (equal (get-event (warrant-name fn) wrld)
                      (make-apply$-warrant-defun-sk fn (formals fn wrld) badge t))
                    (er hard
                      'badge-table-guard
                      "~@0it is claimed that ~x1 has a warrant but ~
                             ~#2~[there is no event introducing a function ~
                             named ~x3~/the event introducing the name ~x3 is ~
                             ~x4 and should be ~x5~]."
                      *badge-table-guard-msg*
                      fn
                      (if (get-event (warrant-name fn) wrld)
                        1
                        0)
                      (warrant-name fn)
                      (get-event (warrant-name fn) wrld)
                      (make-apply$-warrant-defun-sk fn (formals fn wrld) badge t)))
                  (mv-let (erp val)
                    (chk-acceptable-defwarrant1 fn ens wrld)
                    (cond (erp (er hard (cons 'defwarrant fn) "~@0" val))
                      ((eq val t) (er hard
                          (cons 'defwarrant fn)
                          "The function ~x0 is built-in and already has a ~
                             warrant when ACL2 starts up.  It is illegal to ~
                             attempt to ~#1~[add an entry to~/update an entry ~
                             in~] the badge-table for ~x0 in this case.~|~%"
                          fn
                          (if (eq op :new)
                            0
                            1)))
                      (t t))))
                t)))))))
  (defun badge-table-guard
    (key val ens wrld)
    (declare (xargs :mode :program))
    (cond ((not (eq key :badge-userfn-structure)) t)
      (t (badge-table-guard1 val
          (cdr (assoc-eq :badge-userfn-structure (table-alist 'badge-table wrld)))
          ens
          wrld))))
  (set-table-guard badge-table
    (badge-table-guard key val ens world)
    :topic defbadge
    :show t)
  (table badge-table :badge-userfn-structure nil)
  (defun defcong-fn-equal-equal-events
    (term i c1-cn)
    (declare (xargs :guard (and (natp i) (true-listp c1-cn))))
    (cond ((endp c1-cn) nil)
      ((eq (car c1-cn) :fn) (cons `(defcong fn-equal
            equal
            ,TERM
            ,I
            :package :legacy :hints (("Goal" :in-theory (disable (:executable-counterpart force)))))
          (defcong-fn-equal-equal-events term (+ 1 i) (cdr c1-cn))))
      (t (defcong-fn-equal-equal-events term (+ 1 i) (cdr c1-cn)))))
  (defun forced-warrant-fn
    (names)
    (declare (xargs :mode :logic :guard (symbol-listp names)))
    (cond ((endp names) nil)
      ((or (assoc-eq (car names) *badge-prim-falist*)
         (assoc-eq (car names) *apply$-boot-fns-badge-alist*)) (forced-warrant-fn (cdr names)))
      (t (cons (list 'force (list (warrant-name (car names))))
          (forced-warrant-fn (cdr names))))))
  (defmacro warrant
    (&rest names)
    (declare (xargs :guard (symbol-listp names)))
    `(and ,@(FORCED-WARRANT-FN NAMES)))
  (defun chk-acceptable-defwarrant
    (fn ctx ens wrld state)
    (declare (xargs :mode :program))
    (mv-let (msg storedp badge)
      (ok-defbadge fn wrld)
      (declare (ignore storedp))
      (cond (msg (er soft ctx "~@0" msg))
        (t (mv-let (erp val)
            (chk-acceptable-defwarrant1 fn ens wrld)
            (cond (erp (er soft ctx "~@0" val))
              ((eq val t) (value t))
              (t (value (list val badge)))))))))
  (defun confirm-apply-books
    (state)
    (declare (xargs :mode :program))
    (let ((wrld (w state)) (apply-lemmas-book-name *projects/apply/base-sysfile*))
      (cond ((and (not (global-val 'projects/apply/base-includedp wrld))
           (not (equal apply-lemmas-book-name (active-book-name wrld state)))
           (not (global-val 'boot-strap-flg wrld))) (er soft
            'confirm-apply-books
            "Please execute~%~x0~|before the first defun$, defbadge, or ~
           defwarrant.  See :DOC defwarrant."
            '(include-book "projects/apply/top" :dir :system)))
        (t (value nil)))))
  (defun defwarrant-fn1
    (fn state)
    (declare (xargs :mode :program))
    (let ((wrld (w state)))
      (er-progn (confirm-apply-books state)
        (er-let* ((doublet-or-t (chk-acceptable-defwarrant fn
               (cons 'defwarrant fn)
               (ens state)
               wrld
               state)))
          (cond ((eq doublet-or-t t) (pprogn (if (global-val 'boot-strap-flg wrld)
                  state
                  (observation (cons 'defwarrant fn)
                    "The function ~x0 is built-in and already has a warrant when ~
              ACL2 starts up.  This event thus has no effect.~|~%"
                    fn))
                (value `(with-output :stack :pop (value-triple nil)))))
            (t (let ((events (car doublet-or-t)) (badge (cadr doublet-or-t)))
                (value `(encapsulate nil
                    ,@(IF (EQ EVENTS NIL)
      NIL
      `((WITH-OUTPUT :STACK :POP :OFF SUMMARY ,(CAR EVENTS))
        (WITH-OUTPUT :STACK :POP ,(CADR EVENTS))))
                    ,@(DEFWARRANT-EVENTS FN (FORMALS FN WRLD) BADGE)
                    (table badge-table
                      :badge-userfn-structure (put-badge-userfn-structure-tuple-in-alist (make-badge-userfn-structure-tuple ',FN t ',BADGE)
                        (cdr (assoc :badge-userfn-structure (table-alist 'badge-table world)))
                        'defwarrant)
                      :put)
                    ,(IF (GETPROPC FN 'PREDEFINED NIL WRLD)
     `(DEFATTACH (,(WARRANT-NAME FN) TRUE-APPLY$-WARRANT) :SYSTEM-OK T)
     `(DEFATTACH ,(WARRANT-NAME FN) TRUE-APPLY$-WARRANT))
                    ,@(IF (EQ (ACCESS APPLY$-BADGE BADGE :ILKS) T)
      NIL
      (DEFCONG-FN-EQUAL-EQUAL-EVENTS (CONS FN (FORMALS FN WRLD)) 1
                                     (ACCESS APPLY$-BADGE BADGE :ILKS)))
                    (progn ,(IF (GLOBAL-VAL 'BOOT-STRAP-FLG WRLD)
     `(WITH-OUTPUT :STACK :POP
                   (VALUE-TRIPLE
                    (PROG2$
                     (CW "~%~x0 is now warranted by ~x1, with badge ~x2.~%~%"
                         ',FN ',(WARRANT-NAME FN) ',BADGE)
                     :WARRANTED)))
     `(SIDE-EFFECT-EVENT
       (IF (OR (EQ (LD-SKIP-PROOFSP STATE) 'INCLUDE-BOOK)
               (EQ (LD-SKIP-PROOFSP STATE) 'INCLUDE-BOOK-WITH-LOCALS)
               (EQ (LD-SKIP-PROOFSP STATE) 'INITIALIZE-ACL2))
           STATE
           (FMS "~%~x0 is now warranted by ~x1, with badge ~
                                   ~x2.~%~%"
                (LIST (CONS #\0 ',FN) (CONS #\1 ',(WARRANT-NAME FN))
                      (CONS #\2 ',BADGE))
                (STANDARD-CO STATE) STATE NIL))))
                      (with-output :stack :pop (value-triple '(:return-value :warranted) :on-skip-proofs t))))))))))))
  (defun defwarrant-fn
    (fn)
    (declare (xargs :mode :logic :guard t))
    `(defwarrant-fn1 ',FN state))
  (defmacro side-effect-event
    (form)
    `(with-output :off summary
      (make-event (pprogn ,FORM (value '(value-triple :invisible))))))
  (defmacro defwarrant
    (fn)
    `(with-output :off (warning warning!
        observation
        prove
        proof-builder
        event
        history
        summary
        proof-tree)
      :stack :push :gag-mode nil
      (make-event (with-output :stack :pop ,(DEFWARRANT-FN FN))
        :on-behalf-of :quiet!)))
  (defmacro def-warrant
    (fn)
    (er hard
      (msg "~x0" `(def-warrant ,FN))
      "Def-warrant has been replaced by defwarrant.  Please use defwarrant ~
       instead."))
  (defun defbadge-fn1
    (fn state)
    (declare (xargs :mode :program))
    (let ((wrld (w state)) (ctx `(defbadge . ,FN)))
      (er-progn (confirm-apply-books state)
        (mv-let (msg flg badge)
          (ok-defbadge fn wrld)
          (cond (msg (er soft ctx "~@0" msg))
            ((or (apply$-primp fn)
               (assoc-eq fn *apply$-boot-fns-badge-alist*)) (pprogn (if (global-val 'boot-strap-flg wrld)
                  state
                  (observation (cons 'defbadge fn)
                    "The function ~x0 is built-in and already has a badge when ~
              ACL2 starts up.  This event thus has no effect.~|~%"
                    fn))
                (value `(with-output :stack :pop (value-triple nil)))))
            (t (pprogn (cond (flg (cond ((f-get-global 'skip-proofs-by-system state) state)
                      (t (observation (cons 'defbadge fn)
                          "The function ~x0 already has a badge ~
                                       because it is built-in, or because ~
                                       defbadge or defwarrant has been ~
                                       previously invoked on it, or because ~
                                       :loop$-recursion t was declared).  ~
                                       This event thus has no effect.~|~%"
                          fn))))
                  (t (prog2$ (cw "~%~x0 is being given the badge ~x1 but has no warrant.~%~%"
                        fn
                        badge)
                      state)))
                (value `(encapsulate nil
                    (table badge-table
                      :badge-userfn-structure (put-badge-userfn-structure-tuple-in-alist (make-badge-userfn-structure-tuple ',FN nil ',BADGE)
                        (cdr (assoc :badge-userfn-structure (table-alist 'badge-table world)))
                        'defbadge)
                      :put)
                    (with-output :stack :pop (value-triple '(:return-value :badged) :on-skip-proofs t)))))))))))
  (defun defbadge-fn
    (fn)
    (declare (xargs :mode :logic :guard t))
    `(defbadge-fn1 ',FN state))
  (defmacro defbadge
    (fn)
    `(with-output :off (warning warning!
        observation
        prove
        proof-builder
        event
        history
        summary
        proof-tree)
      :stack :push :gag-mode nil
      (make-event (with-output :stack :pop ,(DEFBADGE-FN FN))
        :on-behalf-of :quiet!)))
  (defmacro defun$
    (fn formals &rest rest)
    `(progn (defun ,FN ,FORMALS ,@REST) (defwarrant ,FN)))
  (defmacro defun$!
    (fn formals &rest rest)
    `(progn (defun ,FN
        ,FORMALS
        (declare (xargs :verify-guards nil))
        ,@REST)
      (defwarrant ,FN)
      (verify-guards ,FN)))
  (defattach (badge-userfn doppelganger-badge-userfn)
    (apply$-userfn doppelganger-apply$-userfn)
    :hints (("Goal" :use (doppelganger-badge-userfn-type doppelganger-apply$-userfn-takes-arity-args))))
  (defun until$-ac
    (fn lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil))
          (true-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      ((apply$ fn (list (car lst))) (revappend ac nil))
      (t (until$-ac fn (cdr lst) (cons (car lst) ac)))))
  (defun until$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (if (apply$ fn (list (car lst)))
          nil
          (cons (car lst) (until$ fn (cdr lst)))))
      :exec (until$-ac fn lst nil)))
  (defun until$+-ac
    (fn globals lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      ((apply$ fn (list globals (car lst))) (revappend ac nil))
      (t (until$+-ac fn globals (cdr lst) (cons (car lst) ac)))))
  (defun until$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (if (apply$ fn (list globals (car lst)))
          nil
          (cons (car lst) (until$+ fn globals (cdr lst)))))
      :exec (until$+-ac fn globals lst nil)))
  (defun when$-ac
    (fn lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil))
          (true-listp lst)
          (true-listp ac))
        :mode :program))
    (if (endp lst)
      (revappend ac nil)
      (when$-ac fn
        (cdr lst)
        (if (apply$ fn (list (car lst)))
          (cons (car lst) ac)
          ac))))
  (defun when$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (if (apply$ fn (list (car lst)))
          (cons (car lst) (when$ fn (cdr lst)))
          (when$ fn (cdr lst))))
      :exec (when$-ac fn lst nil)))
  (defun when$+-ac
    (fn globals lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst)
          (true-listp ac))
        :mode :program))
    (if (endp lst)
      (revappend ac nil)
      (when$+-ac fn
        globals
        (cdr lst)
        (if (apply$ fn (list globals (car lst)))
          (cons (car lst) ac)
          ac))))
  (defun when$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (if (apply$ fn (list globals (car lst)))
          (cons (car lst) (when$+ fn globals (cdr lst)))
          (when$+ fn globals (cdr lst))))
      :exec (when$+-ac fn globals lst nil)))
  (defun sum$-ac
    (fn lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil))
          (true-listp lst)
          (acl2-numberp ac))
        :mode :program))
    (if (endp lst)
      ac
      (sum$-ac fn
        (cdr lst)
        (+ (ec-call (the-number (apply$ fn (list (car lst))))) ac))))
  (defun sum$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        0
        (+ (ec-call (the-number (apply$ fn (list (car lst)))))
          (sum$ fn (cdr lst))))
      :exec (sum$-ac fn lst 0)))
  (defun sum$+-ac
    (fn globals lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst)
          (acl2-numberp ac))
        :mode :program))
    (if (endp lst)
      ac
      (sum$+-ac fn
        globals
        (cdr lst)
        (+ (ec-call (the-number (apply$ fn (list globals (car lst)))))
          ac))))
  (defun sum$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        0
        (+ (ec-call (the-number (apply$ fn (list globals (car lst)))))
          (sum$+ fn globals (cdr lst))))
      :exec (sum$+-ac fn globals lst 0)))
  (defun always$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (if (endp lst)
      t
      (if (apply$ fn (list (car lst)))
        (always$ fn (cdr lst))
        nil)))
  (defun always$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (if (endp lst)
      t
      (if (apply$ fn (list globals (car lst)))
        (always$+ fn globals (cdr lst))
        nil)))
  (defun thereis$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (if (endp lst)
      nil
      (or (apply$ fn (list (car lst))) (thereis$ fn (cdr lst)))))
  (defun thereis$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (if (endp lst)
      nil
      (or (apply$ fn (list globals (car lst)))
        (thereis$+ fn globals (cdr lst)))))
  (defun collect$-ac
    (fn lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil))
          (true-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      (t (collect$-ac fn
          (cdr lst)
          (cons (apply$ fn (list (car lst))) ac)))))
  (defun collect$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (cons (apply$ fn (list (car lst))) (collect$ fn (cdr lst))))
      :exec (collect$-ac fn lst nil)))
  (defun collect$+-ac
    (fn globals lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      (t (collect$+-ac fn
          globals
          (cdr lst)
          (cons (apply$ fn (list globals (car lst))) ac)))))
  (defun collect$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (cons (apply$ fn (list globals (car lst)))
          (collect$+ fn globals (cdr lst))))
      :exec (collect$+-ac fn globals lst nil)))
  (defun append$-ac
    (fn lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil))
          (true-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      (t (append$-ac fn
          (cdr lst)
          (ec-call (revappend (apply$ fn (list (car lst))) ac))))))
  (defun append$
    (fn lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil)) (true-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (append (ec-call (the-true-list (apply$ fn (list (car lst)))))
          (append$ fn (cdr lst))))
      :exec (append$-ac fn lst nil)))
  (defun append$+-ac
    (fn globals lst ac)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst)
          (true-listp ac))
        :mode :program))
    (cond ((endp lst) (revappend ac nil))
      (t (append$+-ac fn
          globals
          (cdr lst)
          (revappend (ec-call (the-true-list (apply$ fn (list globals (car lst)))))
            ac)))))
  (defun append$+
    (fn globals lst)
    (declare (xargs :guard (and (apply$-guard fn '(nil nil))
          (true-listp globals)
          (true-list-listp lst))
        :mode :program))
    (mbe :logic (if (endp lst)
        nil
        (append (ec-call (the-true-list (apply$ fn (list globals (car lst)))))
          (append$+ fn globals (cdr lst))))
      :exec (append$+-ac fn globals lst nil)))
  (defun nfix-list
    (list)
    (declare (xargs :guard t))
    (if (consp list)
      (cons (nfix (car list)) (nfix-list (cdr list)))
      nil))
  (defun lexp
    (x)
    (declare (xargs :guard t))
    (or (natp x) (and (consp x) (nat-listp x))))
  (defun lex-fix
    (x)
    (declare (xargs :guard t))
    (cond ((atom x) (nfix x)) (t (nfix-list x))))
  (defun d<
    (x y)
    (declare (xargs :guard (and (nat-listp x) (nat-listp y))))
    (and (consp x)
      (consp y)
      (or (< (car x) (car y))
        (and (= (car x) (car y)) (d< (cdr x) (cdr y))))))
  (defun l<
    (x y)
    (declare (xargs :guard (and (lexp x) (lexp y))))
    (or (< (len x) (len y))
      (and (= (len x) (len y))
        (if (atom x)
          (< x y)
          (d< x y)))))
  (defun loop$-default-values1
    (values alist)
    (declare (xargs :guard t))
    (cond ((atom values) nil)
      (t (cons (cond ((eq (car values) nil) nil)
            ((eq (car values) :df) 0)
            (t (cdr (hons-assoc-equal (car values) alist))))
          (loop$-default-values1 (cdr values) alist)))))
  (defun loop$-default-values
    (values alist)
    (declare (xargs :guard t))
    (cond ((and (consp values) (cdr values)) (loop$-default-values1 values alist))
      (t (car (loop$-default-values1 values alist)))))
  (defun do$
    (measure-fn alist do-fn finally-fn values dolia)
    (declare (xargs :guard (and (apply$-guard measure-fn '(nil))
          (apply$-guard do-fn '(nil))
          (apply$-guard finally-fn '(nil))
          (weak-dolia-p dolia))
        :mode :program :measure (lex-fix (apply$ measure-fn (cons alist 'nil)))
        :well-founded-relation l<))
    (let* ((stobj-values-p (not (all-nils (true-list-fix values)))) (old-measure-value (and stobj-values-p (apply$ measure-fn (list alist))))
        (triple (true-list-fix (apply$ do-fn (list alist))))
        (exit-token (car triple))
        (val (cadr triple))
        (new-alist (caddr triple)))
      (cond ((eq exit-token :return) val)
        ((eq exit-token :loop-finish) (let* ((triple (true-list-fix (apply$ finally-fn (list new-alist)))) (exit-token (car triple))
              (val (cadr triple)))
            (if (eq exit-token :return)
              val
              nil)))
        ((l< (lex-fix (apply$ measure-fn (list new-alist)))
           (lex-fix (if stobj-values-p
               old-measure-value
               (apply$ measure-fn (list alist))))) (do$ measure-fn new-alist do-fn finally-fn values dolia))
        (t (prog2$ (let ((all-stobj-names (true-list-fix (access dolia dolia :all-stobj-names))) (untrans-measure (access dolia dolia :untrans-measure))
                (untrans-do-loop$ (access dolia dolia :untrans-do-loop$)))
              (er hard?
                'do$
                "The measure, ~x0, used in the do loop$ ~
                statement~%~Y12~%failed to decrease!  Recall that do$ tracks ~
                the values of do loop$ variables in an alist.  The measure is ~
                computed using the values in the alist from before and after ~
                execution of the body.  We cannot print the values of double ~
                floats and live stobjs, if any are found in the alist, ~
                because they are raw Lisp objects, not ACL2 objects.  We ~
                print any double float as its corresponding rational and ~
                simply print the name of any live stobj (as a ~
                string).~%~%Before execution of the do body the alist ~
                was~%~Y32.~|After the execution of the do body the alist ~
                was~%~Y42.~|Before the execution of the body the measure ~
                was~%~x5.~|After the execution of the body the measure ~
                was~%~x6.~|~%Logically, in this situation the do$ returns the ~
                value of a term whose output signature is ~x7, where the ~
                value of any component of type :df is #d0.0 and the value of ~
                any stobj component is the last latched value of that stobj."
                untrans-measure
                untrans-do-loop$
                nil
                (eviscerate-do$-alist alist all-stobj-names)
                (eviscerate-do$-alist new-alist all-stobj-names)
                (if stobj-values-p
                  old-measure-value
                  (apply$ measure-fn (list alist)))
                (apply$ measure-fn (list new-alist))
                values))
            (loop$-default-values values new-alist)))))))