		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-appconds

Generate the applicability conditions.

Signature
(defmapping-gen-appconds doma$ domb$ alpha$ beta$ a1...an b1...bm beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$ unconditional$ state) → appconds
Arguments: doma$ — Guard (pseudo-termfnp doma$).; domb$ — Guard (pseudo-termfnp domb$).; alpha$ — Guard (pseudo-termfnp alpha$).; beta$ — Guard (pseudo-termfnp beta$).; a1...an — Guard (symbol-listp a1...an).; b1...bm — Guard (symbol-listp b1...bm).; beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).; alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).; guard-thms$ — Guard (booleanp guard-thms$).; unconditional$ — Guard (booleanp unconditional$).
Returns: appconds — A evmac-appcond-listp.

Definitions and Theorems

Function: defmapping-gen-appconds

(defun defmapping-gen-appconds
       (doma$ domb$ alpha$ beta$ a1...an b1...bm
              beta-of-alpha-thm$ alpha-of-beta-thm$
              guard-thms$ unconditional$ state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termfnp doma$)
                             (pseudo-termfnp domb$)
                             (pseudo-termfnp alpha$)
                             (pseudo-termfnp beta$)
                             (symbol-listp a1...an)
                             (symbol-listp b1...bm)
                             (booleanp beta-of-alpha-thm$)
                             (booleanp alpha-of-beta-thm$)
                             (booleanp guard-thms$)
                             (booleanp unconditional$))))
 (let ((__function__ 'defmapping-gen-appconds))
  (declare (ignorable __function__))
  (b* ((wrld (w state))
       (n (arity doma$ wrld))
       (m (arity domb$ wrld)))
   (append
    (make-evmac-appcond?
     :alpha-image
     (b*
      ((antecedent (apply-term doma$ a1...an))
       (consequent
        (if (= m 1)
            (apply-term* domb$ (apply-term alpha$ a1...an))
          (make-mv-let-call 'mv
                            b1...bm :all (apply-term alpha$ a1...an)
                            (apply-term domb$ b1...bm)))))
      (implicate antecedent consequent)))
    (make-evmac-appcond?
     :beta-image
     (b*
      ((antecedent (apply-term domb$ b1...bm))
       (consequent
         (if (= n 1)
             (apply-term* doma$ (apply-term beta$ b1...bm))
           (make-mv-let-call 'mv
                             a1...an :all (apply-term beta$ b1...bm)
                             (apply-term doma$ a1...an)))))
      (implicate antecedent consequent)))
    (make-evmac-appcond?
     :beta-of-alpha
     (b*
      ((antecedent (if unconditional$ *t*
                     (apply-term doma$ a1...an)))
       (consequent
        (if
         (= n 1)
         (if
           (= m 1)
           (b* ((a (car a1...an)))
             (cons 'equal
                   (cons (apply-term* beta$ (apply-term* alpha$ a))
                         (cons a 'nil))))
          (b*
           ((b1...bm
               (defmapping-differentiate-a/b-vars b1...bm a1...an)))
           (make-mv-let-call
                'mv
                b1...bm
                :all (apply-term* alpha$ (car a1...an))
                (cons 'equal
                      (cons (apply-term beta$ b1...bm)
                            (cons (car a1...an) 'nil))))))
         (if (= m 1)
             (b* ((aa1...aan (defmapping-gen-var-aa/bb a1...an)))
               (make-mv-let-call
                    'mv
                    aa1...aan :all
                    (apply-term* beta$ (apply-term alpha$ a1...an))
                    (conjoin-equalities aa1...aan a1...an)))
          (b*
           ((aa1...aan (defmapping-gen-var-aa/bb a1...an))
            (b1...bm
               (defmapping-differentiate-a/b-vars b1...bm a1...an)))
           (make-mv-let-call
                'mv
                b1...bm :all (apply-term alpha$ a1...an)
                (make-mv-let-call
                     'mv
                     aa1...aan
                     :all (apply-term beta$ b1...bm)
                     (conjoin-equalities aa1...aan a1...an))))))))
      (implicate antecedent consequent))
     :when beta-of-alpha-thm$)
    (make-evmac-appcond?
     :alpha-of-beta
     (b*
      ((antecedent (if unconditional$ *t*
                     (apply-term domb$ b1...bm)))
       (consequent
        (if
         (= n 1)
         (if
           (= m 1)
           (b* ((b (car b1...bm)))
             (cons 'equal
                   (cons (apply-term* alpha$ (apply-term* beta$ b))
                         (cons b 'nil))))
           (b* ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm)))
             (make-mv-let-call
                  'mv
                  bb1...bbm :all
                  (apply-term* alpha$ (apply-term beta$ b1...bm))
                  (conjoin-equalities bb1...bbm b1...bm))))
         (if
          (= m 1)
          (b*
           ((b (car b1...bm))
            (a1...an
               (defmapping-differentiate-a/b-vars a1...an b1...bm)))
           (make-mv-let-call 'mv
                             a1...an :all (apply-term* beta$ b)
                             (cons 'equal
                                   (cons (apply-term alpha$ a1...an)
                                         (cons b 'nil)))))
          (b*
           ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm))
            (a1...an
               (defmapping-differentiate-a/b-vars a1...an b1...bm)))
           (make-mv-let-call
                'mv
                a1...an :all (apply-term beta$ b1...bm)
                (make-mv-let-call
                     'mv
                     bb1...bbm
                     :all (apply-term alpha$ a1...an)
                     (conjoin-equalities bb1...bbm b1...bm))))))))
      (implicate antecedent consequent))
     :when alpha-of-beta-thm$)
    (make-evmac-appcond?
     :doma-guard (cond ((symbolp doma$) (uguard doma$ wrld))
                       (t (term-guard-obligation (lambda-body doma$)
                                                 :limited state)))
     :when guard-thms$)
    (make-evmac-appcond?
     :domb-guard (cond ((symbolp domb$) (uguard domb$ wrld))
                       (t (term-guard-obligation (lambda-body domb$)
                                                 :limited state)))
     :when guard-thms$)
    (make-evmac-appcond?
     :alpha-guard
     (b*
      ((alpha-formals (cond ((symbolp alpha$) (formals alpha$ wrld))
                            (t (lambda-formals alpha$))))
       (alpha-guard
            (cond ((symbolp alpha$) (uguard alpha$ wrld))
                  (t (term-guard-obligation (lambda-body alpha$)
                                            :limited state)))))
      (implicate (apply-term doma$ a1...an)
                 (subcor-var alpha-formals a1...an alpha-guard)))
     :when guard-thms$)
    (make-evmac-appcond?
     :beta-guard
     (b* ((beta-formals (cond ((symbolp beta$) (formals beta$ wrld))
                              (t (lambda-formals beta$))))
          (beta-guard
               (cond ((symbolp beta$) (uguard beta$ wrld))
                     (t (term-guard-obligation (lambda-body beta$)
                                               :limited state)))))
       (implicate (apply-term domb$ b1...bm)
                  (subcor-var beta-formals b1...bm beta-guard)))
     :when guard-thms$)))))