		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-appconds

Generate the applicability conditions.

Signature
(isodata-gen-appconds old$ arg-isomaps res-isomaps predicate$ verify-guards$ wrld) → appconds
Arguments: old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; 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: isodata-gen-appconds

(defun isodata-gen-appconds (old$ arg-isomaps res-isomaps
                                  predicate$ verify-guards$ wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (booleanp predicate$)
                         (booleanp verify-guards$)
                         (plist-worldp wrld))))
 (let ((__function__ 'isodata-gen-appconds))
  (declare (ignorable __function__))
  (b* ((x1...xn (formals old$ wrld))
       (oldp-of-x1...xn
            (isodata-gen-oldp-of-terms x1...xn arg-isomaps))
       (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-isomaps)))
      (if (= m 1)
          (b* ((res-isomap (cdar res-isomaps))
               (oldp-res (isodata-isomap->oldp res-isomap)))
            (implicate oldp-of-x1...xn-conj
                       (fcons-term* oldp-res old-call)))
       (b* ((y1...ym (isodata-gen-result-vars old$ m))
            (oldp-of-y1...ym
                 (isodata-gen-oldp-of-terms y1...ym res-isomaps)))
        (implicate
           oldp-of-x1...xn-conj
           (make-mv-let-call 'mv
                             y1...ym :all
                             old-call (conjoin oldp-of-y1...ym))))))
     :when res-isomaps)
    (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
                                    (isodata-gen-oldp-of-rec-call-args-under-contexts
                                         (recursive-calls old$ wrld)
                                         arg-isomaps))
                         :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$))))))