Process a Java primitive input, or part of an input, of a test for a function call.
(atj-process-test-input-jprim-value input type fn call ctx state) → (mv erp value state)
This is used only if
The
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)