		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-appconds

Generate the applicability conditions.

Signature
(atc-gen-appconds targets wrld) → (mv appconds fn-appconds)
Arguments: targets — Guard (symbol-listp targets).; wrld — Guard (plist-worldp wrld).
Returns: appconds — Type (evmac-appcond-listp appconds).; fn-appconds — Type (symbol-symbol-alistp fn-appconds), given (symbol-listp targets).

Also return an alist from the recursive target functions to the corresponding applicability condition names.

We skip over defstruct names, defobject names, and non-recursive function names.

Definitions and Theorems

Function: atc-gen-appconds

(defun atc-gen-appconds (targets wrld)
  (declare (xargs :guard (and (symbol-listp targets)
                              (plist-worldp wrld))))
  (let ((__function__ 'atc-gen-appconds))
    (declare (ignorable __function__))
    (b* (((when (endp targets)) (mv nil nil))
         (target (car targets))
         ((when (not (function-symbolp target wrld)))
          (atc-gen-appconds (cdr targets) wrld))
         ((when (not (irecursivep+ target wrld)))
          (atc-gen-appconds (cdr targets) wrld))
         (meas (measure+ target wrld))
         (name (packn-pos (list 'natp-of-measure-of- target)
                          :keyword))
         (formula (cons 'natp (cons meas 'nil)))
         (appcond (make-evmac-appcond :name name
                                      :formula formula))
         ((mv appconds fn-appconds)
          (atc-gen-appconds (cdr targets) wrld)))
      (mv (cons appcond appconds)
          (acons target name fn-appconds)))))

Theorem: evmac-appcond-listp-of-atc-gen-appconds.appconds

(defthm evmac-appcond-listp-of-atc-gen-appconds.appconds
  (b* (((mv ?appconds ?fn-appconds)
        (atc-gen-appconds targets wrld)))
    (evmac-appcond-listp appconds))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-gen-appconds.fn-appconds

(defthm symbol-symbol-alistp-of-atc-gen-appconds.fn-appconds
  (implies (symbol-listp targets)
           (b* (((mv ?appconds ?fn-appconds)
                 (atc-gen-appconds targets wrld)))
             (symbol-symbol-alistp fn-appconds)))
  :rule-classes :rewrite)