(atj-gen-shallow-test-code-mv-asgs expr types var-base index) → (mv block vars)
Function:
(defun atj-gen-shallow-test-code-mv-asgs (expr types var-base index) (declare (xargs :guard (and (jexprp expr) (atj-type-listp types) (stringp var-base) (natp index)))) (let ((__function__ 'atj-gen-shallow-test-code-mv-asgs)) (declare (ignorable __function__)) (cond ((endp types) (mv nil nil)) (t (b* ((first-var (str::cat var-base (nat-to-dec-string index))) (first-type (car types)) (first-jtype (atj-type-to-jitype first-type)) (first-expr (jexpr-get-field expr (atj-gen-shallow-mv-field-name index))) (first-block (jblock-locvar first-jtype first-var first-expr)) ((mv rest-block rest-vars) (atj-gen-shallow-test-code-mv-asgs expr (cdr types) var-base (1+ index)))) (mv (append first-block rest-block) (cons first-var rest-vars)))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-mv-asgs.block (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-atj-gen-shallow-test-code-mv-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (string-listp vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-gen-shallow-test-code-mv-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (equal (len vars) (len types))))