		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-test-input

Process the input of a test for a function call.

Signature
(atj-process-test-input input type fn call deep$ guards$ ctx state) → (mv erp test-input state)
Arguments: input — Guard (pseudo-termp input).; type — Guard (atj-typep type).; fn — Just for error messages.
Guard (symbolp fn).; call — Just for error messages.
Guard (pseudo-termp call).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; ctx — Guard (ctxp ctx).
Returns: test-input — Type (atj-test-valuep test-input).

This is some sub-term in of a term (fn ... in ...) specified in the :tests input. The requirements on in, as expained in the user documentation, depend on the :deep and :guards inputs, as well as on the ATJ type assigned to the parameter of fn that corresponds to in: these three values are passed as inputs to this function, which checks these requirements, thus validating in. If the checks succeed, we turn in into the corresponding test value. Note that these checks imply that in is ground.

Definitions and Theorems

Function: atj-process-test-input

(defun atj-process-test-input
       (input type fn call deep$ guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp input)
                             (atj-typep type)
                             (symbolp fn)
                             (pseudo-termp call)
                             (booleanp deep$)
                             (booleanp guards$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-process-test-input))
  (declare (ignorable __function__))
  (b*
   ((irrelevant (atj-test-value-acl2 :irrelevant))
    ((when (or deep$ (not guards$)
               (atj-type-case type :acl2)))
     (if (quotep input)
         (value (atj-test-value-acl2 (unquote-term input)))
      (er-soft+
       ctx t irrelevant
       "The term ~x0 that is an argument of ~
                     the function call (~x1 ...) that translates ~
                     the test term ~x2 in the :TESTS input, ~
                     must be a quoted constant."
       input fn call)))
    ((when (atj-type-case type :jprim))
     (b* ((ptype (atj-type-jprim->get type))
          ((mv erp value state)
           (atj-process-test-input-jprim-value
                input ptype fn call ctx state))
          ((when erp) (mv erp irrelevant state)))
       (value (primitive-type-case
                   ptype
                   :boolean (atj-test-value-jboolean value)
                   :char (atj-test-value-jchar value)
                   :byte (atj-test-value-jbyte value)
                   :short (atj-test-value-jshort value)
                   :int (atj-test-value-jint value)
                   :long (atj-test-value-jlong value)
                   :float (atj-test-value-acl2 :irrelevant)
                   :double (atj-test-value-acl2 :irrelevant)))))
    (ptype (atj-type-jprimarr->comp type))
    ((when (or (primitive-type-case ptype :float)
               (primitive-type-case ptype :double)))
     (er-soft+ ctx t irrelevant
               "Internal error: type of ~x0 arrays not supported."
               ptype))
    (constructor
         (primitive-type-case ptype
                              :boolean 'boolean-array-new-init
                              :char 'char-array-new-init
                              :byte 'byte-array-new-init
                              :short 'short-array-new-init
                              :int 'int-array-new-init
                              :long 'long-array-new-init
                              :float (impossible)
                              :double (impossible)))
    (err-msg
     (msg
      "The term ~x0 that is an argument of ~
                      the function call (~x1 ...) that translates ~
                      the test term ~x2 in the :TESTS input, ~
                      must be a call (~x3 X) where X is ~
                      a translated (LIST ...) term ~
                      (i.e. a nest of CONSes ending with a quoted NIL) ~
                      with fewer than 2^32 terms."
      input fn call constructor))
    ((unless (ffn-symb-p input constructor))
     (er-soft+ ctx t irrelevant "~@0" err-msg))
    (args (fargs input))
    ((unless (= (len args) 1))
     (er-soft+ ctx t irrelevant "~@0" err-msg))
    (arg (car args))
    ((mv okp elements)
     (check-list-call arg))
    ((unless okp)
     (er-soft+ ctx t irrelevant "~@0" err-msg))
    ((mv erp values state)
     (atj-process-test-input-jprim-values
          elements ptype fn input ctx state))
    ((when erp) (mv erp irrelevant state))
    ((unless (< (len values) (expt 2 31)))
     (er-soft+ ctx t irrelevant "~@0" err-msg)))
   (value
    (primitive-type-case
      ptype
      :boolean
      (atj-test-value-jboolean[] (boolean-array-new-init values))
      :char (atj-test-value-jchar[] (char-array-new-init values))
      :byte (atj-test-value-jbyte[] (byte-array-new-init values))
      :short (atj-test-value-jshort[] (short-array-new-init values))
      :int (atj-test-value-jint[] (int-array-new-init values))
      :long (atj-test-value-jlong[] (long-array-new-init values))
      :float irrelevant
      :double irrelevant)))))

Theorem: atj-test-valuep-of-atj-process-test-input.test-input

(defthm atj-test-valuep-of-atj-process-test-input.test-input
  (b*
   (((mv ?erp ?test-input acl2::?state)
     (atj-process-test-input input
                             type fn call deep$ guards$ ctx state)))
   (atj-test-valuep test-input))
  :rule-classes :rewrite)