Adapt a Java expression from source types to destination types.
(atj-adapt-expr-to-types expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$) → (mv block new-expr new-jvar-tmp-index)
If the two lists are singletons, we use atj-adapt-expr-to-type. Otherwise, we are converting a multi-valued expression to another multi-valued expression with the same number of components; here `multi-valued' is in the sense of ACL2's mv. We project the components of the expressions by reading the fields, call atj-adapt-expr-to-type on each of them, and then build a new multi-valued expression with the resulting expressions as arguments. That is, we adapt the expression component-wise.
Unless the starting expression is an expression name, we use an intermediate variable to store the value of the expression before projecting the components; otherwise, we would be re-evaluating the starting expression multiple times. Thus, in general we return a block and an expression, and the index for the temporary variable is threaded though.
Function:
(defun atj-adapt-expr-to-types-aux (expr i n) (declare (xargs :guard (and (jexprp expr) (natp i) (natp n)))) (let ((__function__ 'atj-adapt-expr-to-types-aux)) (declare (ignorable __function__)) (if (or (not (mbt (natp i))) (not (mbt (natp n))) (>= i n)) nil (cons (jexpr-get-field expr (atj-gen-shallow-mv-field-name i)) (atj-adapt-expr-to-types-aux expr (1+ i) n)))))
Theorem:
(defthm jexpr-listp-of-atj-adapt-expr-to-types-aux (b* ((exprs (atj-adapt-expr-to-types-aux expr i n))) (jexpr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-adapt-expr-to-types-aux (b* ((?exprs (atj-adapt-expr-to-types-aux expr i n))) (equal (len exprs) (if (and (natp n) (natp i)) (nfix (- n i)) 0))))
Function:
(defun atj-adapt-expr-to-types (expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$) (declare (xargs :guard (and (jexprp expr) (atj-type-listp src-types) (atj-type-listp dst-types) (stringp jvar-tmp-base) (posp jvar-tmp-index) (booleanp guards$)))) (declare (xargs :guard (and (consp src-types) (consp dst-types) (= (len src-types) (len dst-types))))) (let ((__function__ 'atj-adapt-expr-to-types)) (declare (ignorable __function__)) (b* (((when (= (len src-types) 1)) (mv nil (atj-adapt-expr-to-type expr (car src-types) (car dst-types) guards$) jvar-tmp-index)) (src-jtype (jtype-class (atj-gen-shallow-mv-class-name src-types))) (dst-jtype (jtype-class (atj-gen-shallow-mv-class-name src-types))) ((when (equal src-jtype dst-jtype)) (mv nil (jexpr-fix expr) jvar-tmp-index)) ((mv block expr jvar-tmp-index) (if (jexpr-case expr :name) (mv nil (jexpr-fix expr) jvar-tmp-index) (b* (((mv block var jvar-tmp-index) (atj-gen-jlocvar-indexed src-jtype jvar-tmp-base jvar-tmp-index expr))) (mv block (jexpr-name var) jvar-tmp-index)))) (exprs (atj-adapt-expr-to-types-aux expr 0 (len src-types))) (exprs (atj-adapt-exprs-to-types exprs src-types dst-types guards$))) (mv block (jexpr-smethod dst-jtype *atj-mv-factory-method-name* exprs) jvar-tmp-index))))
Theorem:
(defthm jblockp-of-atj-adapt-expr-to-types.block (b* (((mv common-lisp::?block ?new-expr ?new-jvar-tmp-index) (atj-adapt-expr-to-types expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-adapt-expr-to-types.new-expr (b* (((mv common-lisp::?block ?new-expr ?new-jvar-tmp-index) (atj-adapt-expr-to-types expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$))) (jexprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-adapt-expr-to-types.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?new-expr ?new-jvar-tmp-index) (atj-adapt-expr-to-types expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)