Check that a term does not use any AIJ types.
(atj-check-no-aij-term term fn) → yes/no
The check fails for all quoted constants except:
We disallow calls of the ACL2 functions natively implemented in AIJ, except for equal, if, and not. In the context of the other checks, these do not cause the use of AIJ types. We disallow the Java primitive value deconstructors except boolean-value->bool: the former return AIJ types and thus cause their use; the latter is translated to a no-op in Java, and it is needed to convert ACL2 terms that represent Java booleans to actual ACL2 booleans (e.g. in if tests). We disallow the Java primitive array conversions with lists, because they involve AIJ types. Calls of all the other functions are allowed, in particular the other functions translated to Java, which are all checked to satisfy the requirement of not using AIJ types.
Theorem:
(defthm return-type-of-atj-check-no-aij-term.yes/no (b* ((?yes/no (atj-check-no-aij-term term fn))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-check-no-aij-term-list.yes/no (b* ((?yes/no (atj-check-no-aij-term-list terms fn))) (booleanp yes/no)) :rule-classes :rewrite)