Construct a test value with a given ATJ type.
(atj-test-value-of-type value type) → test-value
Function:
(defun atj-test-value-of-type (value type) (declare (xargs :guard (atj-typep type))) (let ((__function__ 'atj-test-value-of-type)) (declare (ignorable __function__)) (atj-type-case type :jprim (primitive-type-case type.get :boolean (if (boolean-valuep value) (atj-test-value-jboolean value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :char (if (char-valuep value) (atj-test-value-jchar value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :byte (if (byte-valuep value) (atj-test-value-jbyte value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :short (if (short-valuep value) (atj-test-value-jshort value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :int (if (int-valuep value) (atj-test-value-jint value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :long (if (long-valuep value) (atj-test-value-jlong value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :float (prog2$ (raise "Internal error: ~ value ~x0 cannot match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant))) :double (prog2$ (raise "Internal error: ~ value ~x0 cannot match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :jprimarr (primitive-type-case type.comp :boolean (if (boolean-arrayp value) (atj-test-value-jboolean[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :char (if (char-arrayp value) (atj-test-value-jchar[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :byte (if (byte-arrayp value) (atj-test-value-jbyte[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :short (if (short-arrayp value) (atj-test-value-jshort[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :int (if (int-arrayp value) (atj-test-value-jint[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :long (if (long-arrayp value) (atj-test-value-jlong[] value) (prog2$ (raise "Internal error: ~ value ~x0 does not match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :float (prog2$ (raise "Internal error: ~ value ~x0 cannot match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant))) :double (prog2$ (raise "Internal error: ~ value ~x0 cannot match type ~x1." value type) (ec-call (atj-test-value-fix :irrelevant)))) :acl2 (atj-test-value-acl2 value))))
Theorem:
(defthm atj-test-valuep-of-atj-test-value-of-type (b* ((test-value (atj-test-value-of-type value type))) (atj-test-valuep test-value)) :rule-classes :rewrite)
Theorem:
(defthm atj-test-value-of-type-of-atj-type-fix-type (equal (atj-test-value-of-type value (atj-type-fix type)) (atj-test-value-of-type value type)))
Theorem:
(defthm atj-test-value-of-type-atj-type-equiv-congruence-on-type (implies (atj-type-equiv type type-equiv) (equal (atj-test-value-of-type value type) (atj-test-value-of-type value type-equiv))) :rule-classes :congruence)