		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-test

Process a test from the :tests input.

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

The first two arguments of this function are the two components of a pair in the alist computed from :tests. These two components are the name of the test and the call of the test.

We first ensure that the name is a non-empty string consisting only of letters and digits. Then we translate the term (ensuring that the translation succeeds), and we ensure that it has the form (fn in1 in2 ...), where fn is one of the target functions. We check that all the arguments of the function call satisfy the needed requirements (via atj-process-test-inputs), obtaining the corresponding input test values. If the :guards input is t, we ensure that the inputs satisfy the guard of the function. We evaluate the call (fn in1 in2 ...), obtaining either a single result value (if fn is single-valued) or a list of result values (if fn is multi-valued). If :deep is nil and :guards is t, we ensure that the inputs will select an overloaded methods, and we obtain the corresponding output types to contruct the appropriate kind of output test values. We create and return an atj-test record.

Note that a single-valued function may return a list. So we need to look at the number of results returned by the function to recognize the result of the function call from trans-eval as either a single list result or a list of multiple results.

Definitions and Theorems

Function: atj-process-test

(defun atj-process-test (name call 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-test))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-string$
          name
          (msg "The test name ~x0 in the :TESTS input"
               name)
          t nil))
    ((when (equal name ""))
     (er-soft+
      ctx t nil
      "The test name ~x0 in the :TESTS input ~
                             cannot be the empty string."
      name))
    ((unless (chars-in-charset-p (explode name)
                                 (str::letter/digit-chars)))
     (er-soft+
      ctx t nil
      "The test name ~x0 in the :TESTS input ~
                             must contain only letters and digits."
      name))
    ((er (list term$ &))
     (ensure-value-is-untranslated-term$
          call
          (msg "The test term ~x0 in the :TESTS input"
               call)
          t nil))
    ((when (or (variablep term$)
               (fquotep term$)
               (flambda-applicationp term$)))
     (er-soft+
      ctx t nil
      "The test term ~x0 in the :TESTS input ~
                   must translate to ~
                   the call of a named function."
      call))
    (fn (ffn-symb term$))
    ((er &)
     (ensure-value-is-in-list$
      fn targets$
      (msg "among the target functions ~&0."
           targets$)
      (msg
       "The function ~x0 called by ~
                      the test term ~x1 in the :TESTS input"
       fn call)
      t nil))
    (inputs (fargs term$))
    (fn-info (atj-get-function-type-info fn guards$ (w state)))
    (main-fn-type (atj-function-type-info->main fn-info))
    (other-fn-types (atj-function-type-info->others fn-info))
    ((er test-inputs)
     (atj-process-test-inputs
          inputs
          (atj-function-type->inputs main-fn-type)
          fn term$ deep$ guards$ ctx state))
    ((er &)
     (if guards$
      (b* ((guard (subcor-var (formals fn (w state))
                              inputs (uguard fn (w state))))
           ((er (cons & guard-satisfied))
            (trans-eval guard ctx state nil)))
       (if
        (not guard-satisfied)
        (er-soft+
         ctx t nil
         "The test term ~x0 in the :TESTS input ~
                                    must translate to a function call ~
                                    where the guards are satisfied, ~
                                    because the :GUARDS input ~
                                    is (perhaps by default) T."
         call)
        (value nil)))
      (value nil)))
    ((er (cons & output/outputs))
     (trans-eval term$ ctx state nil))
    (nresults (atj-number-of-results fn (w state)))
    ((when (and (>= nresults 2)
                (or (not (true-listp output/outputs))
                    (not (equal (len output/outputs)
                                nresults)))))
     (value
      (raise
       "Internal error: ~
                       the function ~x0 returns ~x1 results, ~
                       but evaluating its call returns ~x2, ~
                       which is not a true list of length ~x1."
       fn nresults output/outputs)))
    (outputs (if (= nresults 1)
                 (list output/outputs)
               output/outputs))
    ((when (or deep$ (not guards$)))
     (b* ((test-outputs (atj-test-value-acl2-list outputs)))
       (value (atj-test name fn test-inputs test-outputs))))
    (in-types (atj-test-values-to-types test-inputs))
    (all-fn-types (cons main-fn-type other-fn-types))
    (fn-type?
       (atj-function-type-of-min-input-types in-types all-fn-types))
    ((when (null fn-type?))
     (value
      (raise
       "Internal error: ~
                       the test term ~x0 in the :TESTS input ~
                       does not have a corresponding Java overloaded method."
       call)))
    (out-types (atj-function-type->outputs fn-type?))
    ((unless (= (len outputs) (len out-types)))
     (value
      (raise
       "Internal error: ~
                       the number of results ~x0 of ~x1 ~
                       does not match the number ~x2 of its output types."
       (len outputs)
       fn (len out-types))))
    (test-outputs (atj-test-values-of-types outputs out-types)))
   (value (atj-test name fn test-inputs test-outputs)))))