		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-appconds

Generate the applicability conditions.

Signature
(expdata-gen-appconds old$ arg-surjmaps res-surjmaps predicate$ verify-guards$ wrld) → appconds
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; predicate$ — Guard (booleanp predicate$).; verify-guards$ — Guard (booleanp verify-guards$).; wrld — Guard (plist-worldp wrld).
Returns: appconds — A evmac-appcond-listp.

Definitions and Theorems

Function: expdata-gen-appconds

(defun expdata-gen-appconds (old$ arg-surjmaps res-surjmaps
                                  predicate$ verify-guards$ wrld)
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (booleanp predicate$)
                        (booleanp verify-guards$)
                        (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-appconds))
  (declare (ignorable __function__))
  (b* ((x1...xn (formals old$ wrld))
       (oldp-of-x1...xn
            (expdata-gen-oldp-of-terms x1...xn arg-surjmaps))
       (oldp-of-x1...xn-conj (conjoin oldp-of-x1...xn))
       (old-guard (uguard old$ wrld))
       (old-call (fcons-term old$ x1...xn)))
   (append
    (make-evmac-appcond?
     :oldp-of-old
     (b* ((m (len res-surjmaps)))
      (if (= m 1)
          (b* ((res-surjmap (cdar res-surjmaps))
               (oldp-res (expdata-surjmap->oldp res-surjmap)))
            (implicate oldp-of-x1...xn-conj
                       (fcons-term* oldp-res old-call)))
       (b* ((y1...ym (expdata-gen-result-vars old$ m))
            (oldp-of-y1...ym
                 (expdata-gen-oldp-of-terms y1...ym res-surjmaps)))
        (implicate
           oldp-of-x1...xn-conj
           (make-mv-let-call 'mv
                             y1...ym :all
                             old-call (conjoin oldp-of-y1...ym))))))
     :when res-surjmaps)
    (make-evmac-appcond?
         :oldp-when-old (implicate old-call oldp-of-x1...xn-conj)
         :when predicate$)
    (make-evmac-appcond? :oldp-of-rec-call-args
                         (implicate oldp-of-x1...xn-conj
                                    (expdata-gen-oldp-of-rec-call-args-under-contexts
                                         (recursive-calls old$ wrld)
                                         arg-surjmaps))
                         :when (irecursivep old$ wrld))
    (make-evmac-appcond?
         :old-guard (implicate old-guard oldp-of-x1...xn-conj)
         :when (and verify-guards$ (not predicate$)))
    (make-evmac-appcond?
         :old-guard-pred (implicate oldp-of-x1...xn-conj old-guard)
         :when (and verify-guards$ predicate$))))))