		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-targets

Process the fn1, ..., fnp inputs.

Signature
(atj-process-targets targets deep guards ctx state) → (mv erp result state)
Arguments: targets — Guard (true-listp targets).; ctx — Guard (ctxp ctx).
Returns: result — Type (null result).

Here we only check fn1, ..., fnp themselves. We collect and check the called functions after checking the remaining inputs; see atj-process-inputs.

Definitions and Theorems

Function: atj-process-targets

(defun atj-process-targets (targets deep guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp targets) (ctxp ctx))))
 (let ((__function__ 'atj-process-targets))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (case (len targets)
      (0
        (er-soft+ ctx t nil
                  "At least one target function must be supplied."))
      (1 (ensure-value-is-function-name$
              (car targets)
              (msg "The target function input ~x0"
                   (car targets))
              t nil))
      (t
       (ensure-list-functions$ targets
                               (msg "The target function inputs ~&0"
                                    targets)
                               t nil))))
    ((er &)
     (ensure-list-has-no-duplicates$
          targets
          (msg "The target functions ~&0" targets)
          t nil))
    ((when (or deep (not guards)))
     (value nil))
    (target-prims
         (intersection-eq
              targets
              (union-eq *atj-jprim-fns* *atj-jprimarr-fns*)))
    ((when (null target-prims))
     (value nil)))
   (er-soft+
    ctx t nil
    "Since the :DEEP input is (perhaps by default) NIL ~
               and the :GUARDS input is (perhaps by default) T, ~
               ~@0."
    (if (= (len target-prims) 1)
        (msg "the function ~x0 cannot be specified as target"
             (car target-prims))
      (msg "the functions ~&0 cannot be specified as targets"))))))

Theorem: null-of-atj-process-targets.result

(defthm null-of-atj-process-targets.result
  (b* (((mv ?erp ?result acl2::?state)
        (atj-process-targets targets deep guards ctx state)))
    (null result))
  :rule-classes :rewrite)