		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-appconds

Generate the applicability conditions.

Signature
(tailrec-gen-appconds old$ test base nonrec combine q r domain$ variant$ verify-guards$ state) → appconds
Arguments: old$ — Guard (symbolp old$).; test — Guard (pseudo-termp test).; base — Guard (pseudo-termp base).; nonrec — Guard (pseudo-termp nonrec).; combine — Guard (pseudo-termp combine).; q — Guard (symbolp q).; r — Guard (symbolp r).; domain$ — Guard (pseudo-termfnp domain$).; variant$ — Guard (tailrec-variantp variant$).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: appconds — A evmac-appcond-listp.

Definitions and Theorems

Function: tailrec-gen-appconds

(defun tailrec-gen-appconds
       (old$ test base nonrec combine q
             r domain$ variant$ verify-guards$ state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp test)
                             (pseudo-termp base)
                             (pseudo-termp nonrec)
                             (pseudo-termp combine)
                             (symbolp q)
                             (symbolp r)
                             (pseudo-termfnp domain$)
                             (tailrec-variantp variant$)
                             (booleanp verify-guards$))))
 (let ((__function__ 'tailrec-gen-appconds))
  (declare (ignorable __function__))
  (b* ((wrld (w state))
       (u (tailrec-gen-var-u old$))
       (v (tailrec-gen-var-v old$))
       (w (tailrec-gen-var-w old$))
       (u1 (tailrec-gen-id-var-u old$ wrld))
       (combine-op (tailrec-gen-combine-op combine q r)))
   (append
    (make-evmac-appcond?
         :domain-of-base (implicate test (apply-term* domain$ base))
         :when (member-eq variant$ '(:monoid :monoid-alt :assoc)))
    (make-evmac-appcond?
         :domain-of-nonrec (implicate (dumb-negate-lit test)
                                      (apply-term* domain$ nonrec))
         :when (member-eq variant$ '(:monoid :assoc)))
    (make-evmac-appcond?
      :domain-of-combine
      (implicate (conjoin2 (apply-term* domain$ u)
                           (apply-term* domain$ v))
                 (apply-term* domain$ (apply-term* combine-op u v)))
      :when (member-eq variant$ '(:monoid :assoc :assoc-alt)))
    (make-evmac-appcond?
         :domain-of-combine-uncond
         (apply-term* domain$ (apply-term* combine-op u v))
         :when (eq variant$ :monoid-alt))
    (make-evmac-appcond?
     :combine-associativity
     (implicate
      (conjoin (list (apply-term* domain$ u)
                     (apply-term* domain$ v)
                     (apply-term* domain$ w)))
      (cons
       'equal
       (cons
          (apply-term* combine-op
                       u (apply-term* combine-op v w))
          (cons (apply-term* combine-op (apply-term* combine-op u v)
                             w)
                'nil))))
     :when (member-eq variant$ '(:monoid :assoc)))
    (make-evmac-appcond?
     :combine-associativity-uncond
     (cons
      'equal
      (cons
          (apply-term* combine-op
                       u (apply-term* combine-op v w))
          (cons (apply-term* combine-op (apply-term* combine-op u v)
                             w)
                'nil)))
     :when (member-eq variant$ '(:monoid-alt :assoc-alt)))
    (make-evmac-appcond?
         :combine-left-identity
         (implicate (conjoin2 test (apply-term* domain$ u1))
                    (cons 'equal
                          (cons (apply-term* combine-op base u1)
                                (cons u1 'nil))))
         :when (member-eq variant$ '(:monoid :monoid-alt)))
    (make-evmac-appcond?
         :combine-right-identity
         (implicate (conjoin2 test (apply-term* domain$ u1))
                    (cons 'equal
                          (cons (apply-term* combine-op u1 base)
                                (cons u1 'nil))))
         :when (member-eq variant$ '(:monoid :monoid-alt)))
    (make-evmac-appcond?
         :domain-guard
         (if (symbolp domain$)
             (guard domain$ nil wrld)
           (term-guard-obligation (lambda-body domain$)
                                  :limited state))
         :when verify-guards$)
    (make-evmac-appcond?
         :combine-guard
         (implicate (conjoin2 (apply-term* domain$ q)
                              (apply-term* domain$ r))
                    (term-guard-obligation combine
                                           :limited state))
         :when verify-guards$)
    (make-evmac-appcond?
         :domain-of-base-when-guard
         (implicate (conjoin2 (guard old$ nil wrld) test)
                    (apply-term* domain$ base))
         :when (and (eq variant$ :assoc-alt)
                    verify-guards$))
    (make-evmac-appcond?
         :domain-of-nonrec-when-guard
         (implicate (conjoin2 (guard old$ nil wrld)
                              (dumb-negate-lit test))
                    (apply-term* domain$ nonrec))
         :when (and (member-eq variant$ '(:monoid-alt :assoc-alt))
                    verify-guards$))))))