Check that an ATJ type is not mapped to an AIJ type.
The allowed ATJ types for this are
This is used on the input and output types of the function passed as argument, which justifies the form of the error message.
If the check fails, we stop with an error.
Function:
(defun atj-check-no-aij-type (type fn) (declare (xargs :guard (and (atj-typep type) (symbolp fn)))) (let ((__function__ 'atj-check-no-aij-type)) (declare (ignorable __function__)) (b* ((pass (atj-type-case type :acl2 (or (atj-atype-case type.get :boolean) (atj-atype-case type.get :character) (atj-atype-case type.get :string)) :jprim t :jprimarr t))) (or pass (raise "The function ~x0 has ~x1 among its input and output types, ~ which violates the checks required by :NO-AIJ-TYPES T. ~ You may need to use JAVA::ATJ-MAIN-FUNCTION-TYPE ~ to record appropriate types for the function ~x0." fn type)))))
Theorem:
(defthm booleanp-of-atj-check-no-aij-type (b* ((yes/no (atj-check-no-aij-type type fn))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm not-atj-check-no-aij-type-of-nil (not (atj-check-no-aij-type nil fn)))