		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-targets

Process the targets t1, ..., tp.

Signature
(atc-process-targets targets wrld) → (mv erp targets target-fns)
Arguments: targets — Guard (true-listp targets).; wrld — Guard (plist-worldp wrld).
Returns: targets — Type (symbol-listp targets).; target-fns — Type (symbol-listp target-fns).

We initialize the lists of previous defstruct targets, previous defobject targets, previous function targets, and uncalled recursive functions to be empty, and we ensure that the latter list is empty after processing all the targets.

We return all the target functions. We also return all the targets, with a guaranteed symbol-listp type for use by the caller.

Definitions and Theorems

Function: atc-process-targets

(defun atc-process-targets (targets wrld)
 (declare (xargs :guard (and (true-listp targets)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-process-targets))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil)
    ((unless (consp targets))
     (reterr "At least one target must be supplied."))
    ((erp targets-as-symbols
          & & previous-fns uncalled-fns)
     (atc-process-target-list targets nil nil nil nil wrld))
    ((unless (endp uncalled-fns))
     (reterr
      (msg
       "The recursive target functions ~&0 ~
                      are not called by any other target function."
       uncalled-fns))))
   (retok targets-as-symbols previous-fns))))

Theorem: symbol-listp-of-atc-process-targets.targets

(defthm symbol-listp-of-atc-process-targets.targets
  (b* (((mv acl2::?erp ?targets ?target-fns)
        (atc-process-targets targets wrld)))
    (symbol-listp targets))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-targets.target-fns

(defthm symbol-listp-of-atc-process-targets.target-fns
  (b* (((mv acl2::?erp ?targets ?target-fns)
        (atc-process-targets targets wrld)))
    (symbol-listp target-fns))
  :rule-classes :rewrite)