		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-test-input-jprim-value

Process a Java primitive input, or part of an input, of a test for a function call.

Signature
(atj-process-test-input-jprim-value input type fn call ctx state) → (mv erp value state)
Arguments: input — Guard (pseudo-termp input).; type — Guard (primitive-typep type).; fn — Just for error messages.
Guard (symbolp fn).; call — Just for error messages.
Guard (pseudo-termp call).; ctx — Guard (ctxp ctx).

This is used only if :deep is nil and :guards is t.

The input argument could be a sub-term in of a term (fn ... in ...) specified in the :tests input when that argument of fn has a Java primitive type, or it could be a further sub-term of such an in sub-term when the latter denotes a Java primitive array.

Definitions and Theorems

Function: atj-process-test-input-jprim-value

(defun atj-process-test-input-jprim-value
       (input type fn call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp input)
                             (primitive-typep type)
                             (symbolp fn)
                             (pseudo-termp call)
                             (ctxp ctx))))
 (let ((__function__ 'atj-process-test-input-jprim-value))
  (declare (ignorable __function__))
  (b*
   (((when (member-eq (primitive-type-kind type)
                      '(:float :double)))
     (er-soft+ ctx t nil
               "Internal error: type ~x0 not supported."
               type))
    (irrelevant (primitive-type-case type
                                     :boolean (boolean-value nil)
                                     :char (char-value 0)
                                     :byte (byte-value 0)
                                     :short (short-value 0)
                                     :int (int-value 0)
                                     :long (long-value 0)
                                     :float (impossible)
                                     :double (impossible)))
    (constructor (primitive-type-case type
                                      :boolean 'boolean-value
                                      :char 'char-value
                                      :byte 'byte-value
                                      :short 'short-value
                                      :int 'int-value
                                      :long 'long-value
                                      :float nil
                                      :double nil))
    (err-msg
     (msg
      "The term ~x0 that is (possibly part of) 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 ~s4."
      input fn call constructor
      (primitive-type-case type
                           :boolean "a boolean"
                           :char "an unsigned 16-bit integer"
                           :byte "a signed 8-bit integer"
                           :short "a signed 16-bit integer"
                           :int "a signed 32-bit integer"
                           :long "a signed 64-bit integer"
                           :float nil
                           :double nil)))
    ((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))
    ((unless (quotep arg))
     (er-soft+ ctx t irrelevant "~@0" err-msg))
    (arg (unquote-term arg))
    ((unless (primitive-type-case type
                                  :boolean (booleanp arg)
                                  :char (ubyte16p arg)
                                  :byte (sbyte8p arg)
                                  :short (sbyte16p arg)
                                  :int (sbyte32p arg)
                                  :long (sbyte64p arg)
                                  :float nil
                                  :double nil))
     (er-soft+ ctx t irrelevant "~@0" err-msg)))
   (value (primitive-type-case type
                               :boolean (boolean-value arg)
                               :char (char-value arg)
                               :byte (byte-value arg)
                               :short (short-value arg)
                               :int (int-value arg)
                               :long (long-value arg)
                               :float nil
                               :double nil)))))

Theorem: boolean-valuep-of-atj-process-test-input-jprim-value.value

(defthm boolean-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :boolean)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (boolean-valuep value)))
  :rule-classes :rewrite)

Theorem: char-valuep-of-atj-process-test-input-jprim-value.value

(defthm char-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :char)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (char-valuep value)))
  :rule-classes :rewrite)

Theorem: byte-valuep-of-atj-process-test-input-jprim-value.value

(defthm byte-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :byte)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (byte-valuep value)))
  :rule-classes :rewrite)

Theorem: short-valuep-of-atj-process-test-input-jprim-value.value

(defthm short-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :short)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (short-valuep value)))
  :rule-classes :rewrite)

Theorem: int-valuep-of-atj-process-test-input-jprim-value.value

(defthm int-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :int)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (int-valuep value)))
  :rule-classes :rewrite)

Theorem: long-valuep-of-atj-process-test-input-jprim-value.value

(defthm long-valuep-of-atj-process-test-input-jprim-value.value
  (implies (primitive-type-case type :long)
           (b* (((mv ?erp acl2::?value acl2::?state)
                 (atj-process-test-input-jprim-value
                      input type fn call ctx state)))
             (long-valuep value)))
  :rule-classes :rewrite)