Generate a Java type, in the shallow embedding approach.
(atj-gen-shallow-jtype types) → jtype
We map a non-empty list of ATJ types to a Java type as follows. If the list is a singleton, we map the (only) type to the corresponding Java type, according to atj-type-to-jitype. Otherwise, we map the list of two or more types to the mv class for the types, according to atj-gen-shallow-mv-class-name.
Function:
(defun atj-gen-shallow-jtype (types) (declare (xargs :guard (atj-type-listp types))) (declare (xargs :guard (consp types))) (let ((__function__ 'atj-gen-shallow-jtype)) (declare (ignorable __function__)) (if (= (len types) 1) (atj-type-to-jitype (car types)) (jtype-class (atj-gen-shallow-mv-class-name types)))))
Theorem:
(defthm jtypep-of-atj-gen-shallow-jtype (b* ((jtype (atj-gen-shallow-jtype types))) (jtypep jtype)) :rule-classes :rewrite)