		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-tests

Process the :tests input.

Signature
(atj-process-tests tests targets$ deep$ guards$ ctx state) → (mv erp tests$ state)
Arguments: targets$ — Guard (symbol-listp targets$).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; ctx — Guard (ctxp ctx).
Returns: tests$ — An atj-test-listp.

After evaluating :tests and ensuring that the result is a list of doublets, we convert it into an alist and we ensure that the keys are unique. Then we process each pair in the alist, via an auxiliary function.

Definitions and Theorems

Function: atj-process-tests-aux

(defun atj-process-tests-aux
       (tests-alist targets$ deep$ guards$ ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (alistp tests-alist)
                              (symbol-listp targets$)
                              (booleanp deep$)
                              (booleanp guards$)
                              (ctxp ctx))))
  (let ((__function__ 'atj-process-tests-aux))
    (declare (ignorable __function__))
    (b* (((when (endp tests-alist)) (value nil))
         ((cons (cons name call) tests-alist)
          tests-alist)
         ((er test$)
          (atj-process-test name
                            call targets$ deep$ guards$ ctx state))
         ((er tests$)
          (atj-process-tests-aux tests-alist
                                 targets$ deep$ guards$ ctx state)))
      (value (cons test$ tests$)))))

Function: atj-process-tests

(defun atj-process-tests (tests targets$ deep$ guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp targets$)
                             (booleanp deep$)
                             (booleanp guards$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-process-tests))
  (declare (ignorable __function__))
  (b*
   (((er (cons & tests))
     (trans-eval tests ctx state nil))
    (description "The :TESTS input")
    ((er &)
     (ensure-doublet-list$ tests description t nil))
    (alist (doublets-to-alist tests))
    (names (strip-cars alist))
    (description
       (msg "The list ~x0 of names of the tests in the :TESTS input"
            names))
    ((er &)
     (ensure-list-has-no-duplicates$ names description t nil)))
   (atj-process-tests-aux alist
                          targets$ deep$ guards$ ctx state))))